perm filename RSA.PRO[BMP,SYS] blob
sn#737851 filedate 1984-01-17 generic text, type T, neo UTF8
January 17, 1984 21:16:55
(NOTE-LIB PROVEALL.LIB PROVEALL.LISP)
[ 24.068 0.0 ]
#FILE-IN-|DSK:PROVEA.LIB[BM,CLT]|-71764
(DISABLE EUCLID)
[ 0.167999776 0.0 ]
G0002
(DISABLE QUOTIENT-DIVIDES)
[ 0.113999939 0.0 ]
G0003
(DISABLE IF-TIMES-THEN-DIVIDES)
[ 0.087000021 0.0 ]
G0004
(DISABLE TIMES)
[ 0.308000185 0.0 ]
G0005
(DEFN CRYPT
(M E N)
(IF
(ZEROP E)
1.
(IF
(EVEN E)
(REMAINDER (SQUARE (CRYPT M (QUOTIENT E 2.) N))
N)
(REMAINDER (TIMES M
(REMAINDER (SQUARE (CRYPT M (QUOTIENT E 2.) N))
N))
N))))
The lemmas LESSP-QUOTIENT1 and COUNT-NUMBERP and the definitions
of NUMBERP, EQUAL, EVEN, and ZEROP can be used to prove that the
measure (COUNT E) decreases according to the well-founded relation
LESSP in each recursive call. Hence, CRYPT is accepted under the
principle of definition. Observe that (NUMBERP (CRYPT M E N)) is a
theorem.
[ 10.4569997 0.582000226 ]
CRYPT
(PROVE-LEMMA TIMES-MOD-1
(REWRITE)
(EQUAL (REMAINDER (TIMES X (REMAINDER Y N))
N)
(REMAINDER (TIMES X Y) N)))
.
Appealing to the lemma REMAINDER-QUOTIENT-ELIM, we now replace Y by
(PLUS Z (TIMES N V)) to eliminate (REMAINDER Y N) and (QUOTIENT Y N).
We rely upon LESSP-REMAINDER2, the type restriction lemma noted when
REMAINDER was introduced, and the type restriction lemma noted when
QUOTIENT was introduced to restrict the new variables. This produces
the following four new goals:
Case 4. (IMPLIES (NOT (NUMBERP Y))
(EQUAL (REMAINDER (TIMES X (REMAINDER Y N))
N)
(REMAINDER (TIMES X Y) N))),
which simplifies, rewriting with COMMUTATIVITY-OF-TIMES,
TIMES-IDENTITY, TIMES-ZERO2, and REMAINDER-0-CROCK, and expanding
the functions LESSP, REMAINDER, and EQUAL, to:
T.
Case 3. (IMPLIES (EQUAL N 0)
(EQUAL (REMAINDER (TIMES X (REMAINDER Y N))
N)
(REMAINDER (TIMES X Y) N))),
which we simplify, expanding the functions EQUAL and REMAINDER, to:
(IMPLIES (NOT (NUMBERP Y))
(EQUAL (TIMES X 0) (TIMES X Y))),
which we again simplify, rewriting with COMMUTATIVITY-OF-TIMES,
TIMES-ZERO2, and TIMES-IDENTITY, and unfolding the function EQUAL,
to:
T.
Case 2. (IMPLIES (NOT (NUMBERP N))
(EQUAL (REMAINDER (TIMES X (REMAINDER Y N))
N)
(REMAINDER (TIMES X Y) N))).
But this simplifies, applying REMAINDER-WRT-12, to:
(IMPLIES (AND (NOT (NUMBERP N))
(NOT (NUMBERP Y)))
(EQUAL (TIMES X 0) (TIMES X Y))),
which we again simplify, rewriting with the lemmas
COMMUTATIVITY-OF-TIMES, TIMES-ZERO2, and TIMES-IDENTITY, and
expanding the definition of EQUAL, to:
T.
Case 1. (IMPLIES (AND (NUMBERP Z)
(EQUAL (LESSP Z N) (NOT (ZEROP N)))
(NUMBERP V)
(NUMBERP N)
(NOT (EQUAL N 0)))
(EQUAL (REMAINDER (TIMES X Z) N)
(REMAINDER (TIMES X (PLUS Z (TIMES N V)))
N))),
which we simplify, rewriting with the lemmas COMMUTATIVITY-OF-TIMES,
COMMUTATIVITY2-OF-TIMES, DISTRIBUTIVITY-OF-TIMES-OVER-PLUS, and
REMAINDER-PLUS-TIMES-2, and unfolding ZEROP and NOT, to:
T.
Q.E.D.
[ 12.1520004 1.21400045 ]
TIMES-MOD-1
(PROVE-LEMMA TIMES-MOD-2
(REWRITE)
(EQUAL (REMAINDER (TIMES A (TIMES B (REMAINDER Y N)))
N)
(REMAINDER (TIMES A B Y) N))
((USE (TIMES-MOD-1 (X (TIMES A B))))
(DISABLE TIMES-MOD-1)))
This formula can be simplified, using the abbreviation
ASSOCIATIVITY-OF-TIMES, to:
T.
This simplifies, trivially, to:
T.
Q.E.D.
[ 0.23600362 0.0249969482 ]
TIMES-MOD-2
(PROVE-LEMMA CRYPT-CORRECT
(REWRITE)
(IMPLIES (NOT (EQUAL N 1.))
(EQUAL (CRYPT M E N)
(REMAINDER (EXP M E) N))))
Name the conjecture *1.
We will try to prove it by induction. There are two plausible
inductions, both of which are unflawed. So we will choose the one
suggested by the largest number of nonprimitive recursive functions.
We will induct according to the following scheme:
(AND (IMPLIES (ZEROP E) (P M E N))
(IMPLIES (AND (NOT (ZEROP E))
(EVEN E)
(P M (QUOTIENT E 2) N))
(P M E N))
(IMPLIES (AND (NOT (ZEROP E))
(NOT (EVEN E))
(P M (QUOTIENT E 2) N))
(P M E N))).
The lemmas LESSP-QUOTIENT1 and COUNT-NUMBERP and the definitions of
NUMBERP, EQUAL, EVEN, and ZEROP inform us that the measure (COUNT E)
decreases according to the well-founded relation LESSP in each
induction step of the scheme. The above induction scheme generates
the following three new formulas:
Case 3. (IMPLIES (AND (ZEROP E) (NOT (EQUAL N 1)))
(EQUAL (CRYPT M E N)
(REMAINDER (EXP M E) N))),
which simplifies, applying EXP-BY-0 and REMAINDER-OF-1, and
expanding the definitions of ZEROP, EQUAL, CRYPT, and EXP, to:
T.
Case 2. (IMPLIES (AND (NOT (ZEROP E))
(EVEN E)
(EQUAL (CRYPT M (QUOTIENT E 2) N)
(REMAINDER (EXP M (QUOTIENT E 2)) N))
(NOT (EQUAL N 1)))
(EQUAL (CRYPT M E N)
(REMAINDER (EXP M E) N))),
which simplifies, unfolding the functions ZEROP, EVEN, CRYPT, EQUAL,
and SQUARE, to:
(IMPLIES (AND (NOT (EQUAL E 0))
(NUMBERP E)
(EQUAL 0 (REMAINDER E 2))
(EQUAL (CRYPT M (QUOTIENT E 2) N)
(REMAINDER (EXP M (QUOTIENT E 2)) N))
(NOT (EQUAL N 1)))
(EQUAL (REMAINDER (TIMES (CRYPT M (QUOTIENT E 2) N)
(CRYPT M (QUOTIENT E 2) N))
N)
(REMAINDER (EXP M E) N))).
Applying the lemma REMAINDER-QUOTIENT-ELIM, replace E by
(PLUS X (TIMES 2 Z)) to eliminate (REMAINDER E 2) and
(QUOTIENT E 2). We use LESSP-REMAINDER2, the type restriction
lemma noted when REMAINDER was introduced, and the type restriction
lemma noted when QUOTIENT was introduced to restrict the new
variables. This produces the following three new formulas:
Case 2.3.
(IMPLIES
(AND (EQUAL 2 0)
(NOT (EQUAL E 0))
(NUMBERP E)
(EQUAL 0 (REMAINDER E 2))
(EQUAL (CRYPT M (QUOTIENT E 2) N)
(REMAINDER (EXP M (QUOTIENT E 2)) N))
(NOT (EQUAL N 1)))
(EQUAL (REMAINDER (TIMES (CRYPT M (QUOTIENT E 2) N)
(CRYPT M (QUOTIENT E 2) N))
N)
(REMAINDER (EXP M E) N))),
which we further simplify, using linear arithmetic, to:
T.
Case 2.2.
(IMPLIES
(AND (NOT (NUMBERP 2))
(NOT (EQUAL E 0))
(NUMBERP E)
(EQUAL 0 (REMAINDER E 2))
(EQUAL (CRYPT M (QUOTIENT E 2) N)
(REMAINDER (EXP M (QUOTIENT E 2)) N))
(NOT (EQUAL N 1)))
(EQUAL (REMAINDER (TIMES (CRYPT M (QUOTIENT E 2) N)
(CRYPT M (QUOTIENT E 2) N))
N)
(REMAINDER (EXP M E) N))),
which we further simplify, clearly, to:
T.
Case 2.1.
(IMPLIES
(AND (NUMBERP X)
(EQUAL (LESSP X 2) (NOT (ZEROP 2)))
(NUMBERP Z)
(NOT (EQUAL 2 0))
(NOT (EQUAL (PLUS X (TIMES 2 Z)) 0))
(EQUAL 0 X)
(EQUAL (CRYPT M Z N)
(REMAINDER (EXP M Z) N))
(NOT (EQUAL N 1)))
(EQUAL (REMAINDER (TIMES (CRYPT M Z N) (CRYPT M Z N))
N)
(REMAINDER (EXP M (PLUS X (TIMES 2 Z)))
N))).
This simplifies further, rewriting with the lemmas TIMES-2,
CORRECTNESS-OF-CANCEL, PLUS-EQUAL-0, EXP-BY-0, EXP-PLUS, and
TIMES-1, and unfolding NUMBERP, LESSP, ZEROP, NOT, and EQUAL, to:
(IMPLIES
(AND (NUMBERP Z)
(NOT (EQUAL Z 0))
(EQUAL (CRYPT M Z N)
(REMAINDER (EXP M Z) N))
(NOT (EQUAL N 1)))
(EQUAL (REMAINDER (TIMES (CRYPT M Z N) (CRYPT M Z N))
N)
(REMAINDER (TIMES (EXP M Z) (EXP M Z))
N))).
We use the above equality hypothesis by substituting
(REMAINDER (EXP M Z) N) for (CRYPT M Z N) and throwing away the
equality. This produces:
(IMPLIES (AND (NUMBERP Z)
(NOT (EQUAL Z 0))
(NOT (EQUAL N 1)))
(EQUAL (REMAINDER (TIMES (REMAINDER (EXP M Z) N)
(REMAINDER (EXP M Z) N))
N)
(REMAINDER (TIMES (EXP M Z) (EXP M Z))
N))).
But this simplifies further, applying COMMUTATIVITY-OF-TIMES and
TIMES-MOD-1, to:
T.
Case 1. (IMPLIES (AND (NOT (ZEROP E))
(NOT (EVEN E))
(EQUAL (CRYPT M (QUOTIENT E 2) N)
(REMAINDER (EXP M (QUOTIENT E 2)) N))
(NOT (EQUAL N 1)))
(EQUAL (CRYPT M E N)
(REMAINDER (EXP M E) N))),
which we simplify, rewriting with TIMES-MOD-1, and expanding the
functions ZEROP, EVEN, CRYPT, and SQUARE, to:
(IMPLIES
(AND (NOT (EQUAL E 0))
(NUMBERP E)
(NOT (EQUAL 0 (REMAINDER E 2)))
(EQUAL (CRYPT M (QUOTIENT E 2) N)
(REMAINDER (EXP M (QUOTIENT E 2)) N))
(NOT (EQUAL N 1)))
(EQUAL (REMAINDER (TIMES M
(TIMES (CRYPT M (QUOTIENT E 2) N)
(CRYPT M (QUOTIENT E 2) N)))
N)
(REMAINDER (EXP M E) N))),
which we again simplify, using linear arithmetic, rewriting with
the lemma LESSP-REMAINDER-DIVISOR, and expanding the definition of
EQUAL, to the new conjecture:
(IMPLIES
(AND (EQUAL (REMAINDER E 2) 1)
(NOT (EQUAL E 0))
(NUMBERP E)
(NOT (EQUAL 0 1))
(EQUAL (CRYPT M (QUOTIENT E 2) N)
(REMAINDER (EXP M (QUOTIENT E 2)) N))
(NOT (EQUAL N 1)))
(EQUAL (REMAINDER (TIMES M
(TIMES (CRYPT M (QUOTIENT E 2) N)
(CRYPT M (QUOTIENT E 2) N)))
N)
(REMAINDER (EXP M E) N))),
which again simplifies, expanding the function EQUAL, to the
conjecture:
(IMPLIES
(AND (EQUAL (REMAINDER E 2) 1)
(NOT (EQUAL E 0))
(NUMBERP E)
(EQUAL (CRYPT M (QUOTIENT E 2) N)
(REMAINDER (EXP M (QUOTIENT E 2)) N))
(NOT (EQUAL N 1)))
(EQUAL (REMAINDER (TIMES M
(TIMES (CRYPT M (QUOTIENT E 2) N)
(CRYPT M (QUOTIENT E 2) N)))
N)
(REMAINDER (EXP M E) N))).
Applying the lemma REMAINDER-QUOTIENT-ELIM, replace E by
(PLUS X (TIMES 2 Z)) to eliminate (REMAINDER E 2) and
(QUOTIENT E 2). We rely upon LESSP-REMAINDER2, the type
restriction lemma noted when REMAINDER was introduced, and the type
restriction lemma noted when QUOTIENT was introduced to constrain
the new variables. We would thus like to prove three new goals:
Case 1.3.
(IMPLIES
(AND (EQUAL 2 0)
(EQUAL (REMAINDER E 2) 1)
(NOT (EQUAL E 0))
(NUMBERP E)
(EQUAL (CRYPT M (QUOTIENT E 2) N)
(REMAINDER (EXP M (QUOTIENT E 2)) N))
(NOT (EQUAL N 1)))
(EQUAL
(REMAINDER (TIMES M
(TIMES (CRYPT M (QUOTIENT E 2) N)
(CRYPT M (QUOTIENT E 2) N)))
N)
(REMAINDER (EXP M E) N))),
which we further simplify, using linear arithmetic, to:
T.
Case 1.2.
(IMPLIES
(AND (NOT (NUMBERP 2))
(EQUAL (REMAINDER E 2) 1)
(NOT (EQUAL E 0))
(NUMBERP E)
(EQUAL (CRYPT M (QUOTIENT E 2) N)
(REMAINDER (EXP M (QUOTIENT E 2)) N))
(NOT (EQUAL N 1)))
(EQUAL
(REMAINDER (TIMES M
(TIMES (CRYPT M (QUOTIENT E 2) N)
(CRYPT M (QUOTIENT E 2) N)))
N)
(REMAINDER (EXP M E) N))),
which we further simplify, trivially, to:
T.
Case 1.1.
(IMPLIES
(AND (NUMBERP X)
(EQUAL (LESSP X 2) (NOT (ZEROP 2)))
(NUMBERP Z)
(NOT (EQUAL 2 0))
(EQUAL X 1)
(NOT (EQUAL (PLUS X (TIMES 2 Z)) 0))
(EQUAL (CRYPT M Z N)
(REMAINDER (EXP M Z) N))
(NOT (EQUAL N 1)))
(EQUAL
(REMAINDER (TIMES M
(TIMES (CRYPT M Z N) (CRYPT M Z N)))
N)
(REMAINDER (EXP M (PLUS X (TIMES 2 Z)))
N))),
which we further simplify, rewriting with TIMES-2, PLUS-EQUAL-0,
COMMUTATIVITY-OF-TIMES, TIMES-1, EXP-BY-0, EXP-PLUS, and
COMMUTATIVITY2-OF-TIMES, and opening up the functions NUMBERP,
LESSP, ZEROP, NOT, EQUAL, SUB1, and EXP, to two new goals:
Case 1.1.2.
(IMPLIES
(AND (NUMBERP Z)
(EQUAL (CRYPT M Z N)
(REMAINDER (EXP M Z) N))
(NOT (EQUAL N 1))
(NOT (NUMBERP M)))
(EQUAL
(REMAINDER (TIMES M
(TIMES (CRYPT M Z N) (CRYPT M Z N)))
N)
(REMAINDER (TIMES (EXP M Z) (TIMES (EXP M Z) 0))
N))).
But this again simplifies, rewriting with the lemmas
EQUAL-TIMES-0, COMMUTATIVITY-OF-TIMES, COMMUTATIVITY2-OF-TIMES,
and TIMES-IDENTITY, and expanding the definitions of LESSP,
REMAINDER, and EQUAL, to:
(IMPLIES
(AND (NUMBERP Z)
(EQUAL (CRYPT M Z N)
(REMAINDER (EXP M Z) N))
(NOT (EQUAL N 1))
(NOT (NUMBERP M)))
(EQUAL (TIMES M
(TIMES (CRYPT M Z N) (CRYPT M Z N)))
(TIMES 0
(TIMES (EXP M Z) (EXP M Z))))).
We use the above equality hypothesis by substituting
(REMAINDER (EXP M Z) N) for (CRYPT M Z N) and throwing away the
equality. The result is the conjecture:
(IMPLIES (AND (NUMBERP Z)
(NOT (EQUAL N 1))
(NOT (NUMBERP M)))
(EQUAL (TIMES M
(TIMES (REMAINDER (EXP M Z) N)
(REMAINDER (EXP M Z) N)))
(TIMES 0
(TIMES (EXP M Z) (EXP M Z))))).
We will try to prove the above formula by generalizing it,
replacing (EXP M Z) by Y. We restrict the new variable by
appealing to the type restriction lemma noted when EXP was
introduced. We thus obtain:
(IMPLIES (AND (NUMBERP Y)
(NUMBERP Z)
(NOT (EQUAL N 1))
(NOT (NUMBERP M)))
(EQUAL (TIMES M
(TIMES (REMAINDER Y N)
(REMAINDER Y N)))
(TIMES 0 (TIMES Y Y)))).
Appealing to the lemma REMAINDER-QUOTIENT-ELIM, replace Y by
(PLUS X (TIMES N V)) to eliminate (REMAINDER Y N) and
(QUOTIENT Y N). We use LESSP-REMAINDER2, the type restriction
lemma noted when REMAINDER was introduced, and the type
restriction lemma noted when QUOTIENT was introduced to
restrict the new variables. This produces the following three
new conjectures:
Case 1.1.2.3.
(IMPLIES (AND (EQUAL N 0)
(NUMBERP Y)
(NUMBERP Z)
(NOT (EQUAL N 1))
(NOT (NUMBERP M)))
(EQUAL (TIMES M
(TIMES (REMAINDER Y N)
(REMAINDER Y N)))
(TIMES 0 (TIMES Y Y)))),
which further simplifies, expanding the functions EQUAL and
REMAINDER, to the new conjecture:
(IMPLIES (AND (NUMBERP Y)
(NUMBERP Z)
(NOT (NUMBERP M)))
(EQUAL (TIMES M (TIMES Y Y))
(TIMES 0 (TIMES Y Y)))).
We will try to prove the above conjecture by generalizing it,
replacing (TIMES Y Y) by A. We restrict the new variable by
appealing to the type restriction lemma noted when TIMES was
introduced. We would thus like to prove the new formula:
(IMPLIES (AND (NUMBERP A)
(NUMBERP Y)
(NUMBERP Z)
(NOT (NUMBERP M)))
(EQUAL (TIMES M A) (TIMES 0 A))).
But this finally simplifies, rewriting with TIMES-ZERO2,
COMMUTATIVITY-OF-TIMES, and TIMES-IDENTITY, and expanding
EQUAL, to:
T.
Case 1.1.2.2.
(IMPLIES (AND (NOT (NUMBERP N))
(NUMBERP Y)
(NUMBERP Z)
(NOT (EQUAL N 1))
(NOT (NUMBERP M)))
(EQUAL (TIMES M
(TIMES (REMAINDER Y N)
(REMAINDER Y N)))
(TIMES 0 (TIMES Y Y)))).
But this further simplifies, rewriting with REMAINDER-WRT-12,
to:
(IMPLIES (AND (NOT (NUMBERP N))
(NUMBERP Y)
(NUMBERP Z)
(NOT (NUMBERP M)))
(EQUAL (TIMES M (TIMES Y Y))
(TIMES 0 (TIMES Y Y)))).
We will try to prove the above formula by generalizing it,
replacing (TIMES Y Y) by A. We restrict the new variable by
appealing to the type restriction lemma noted when TIMES was
introduced. We must thus prove:
(IMPLIES (AND (NUMBERP A)
(NOT (NUMBERP N))
(NUMBERP Y)
(NUMBERP Z)
(NOT (NUMBERP M)))
(EQUAL (TIMES M A) (TIMES 0 A))).
This finally simplifies, rewriting with TIMES-ZERO2,
COMMUTATIVITY-OF-TIMES, and TIMES-IDENTITY, and opening up
EQUAL, to:
T.
Case 1.1.2.1.
(IMPLIES (AND (NUMBERP X)
(EQUAL (LESSP X N) (NOT (ZEROP N)))
(NUMBERP V)
(NUMBERP N)
(NOT (EQUAL N 0))
(NUMBERP Z)
(NOT (EQUAL N 1))
(NOT (NUMBERP M)))
(EQUAL (TIMES M (TIMES X X))
(TIMES 0
(TIMES (PLUS X (TIMES N V))
(PLUS X (TIMES N V)))))),
which further simplifies, rewriting with
COMMUTATIVITY-OF-TIMES, COMMUTATIVITY2-OF-TIMES,
DISTRIBUTIVITY-OF-TIMES-OVER-PLUS, ASSOCIATIVITY-OF-PLUS, and
TIMES-IDENTITY, and expanding ZEROP, NOT, EQUAL, and PLUS, to:
(IMPLIES
(AND (NUMBERP X)
(LESSP X N)
(NUMBERP V)
(NUMBERP N)
(NOT (EQUAL N 0))
(NUMBERP Z)
(NOT (EQUAL N 1))
(NOT (NUMBERP M)))
(EQUAL (TIMES M (TIMES X X))
(TIMES 0
(TIMES N (TIMES N (TIMES V V)))))),
which has an irrelevant term in it. By eliminating the term
we get:
(IMPLIES
(AND (NUMBERP X)
(LESSP X N)
(NUMBERP V)
(NUMBERP N)
(NOT (EQUAL N 0))
(NOT (EQUAL N 1))
(NOT (NUMBERP M)))
(EQUAL (TIMES M (TIMES X X))
(TIMES 0
(TIMES N (TIMES N (TIMES V V)))))).
Finally give the above formula the name *1.1.
Case 1.1.1.
(IMPLIES
(AND (NUMBERP Z)
(EQUAL (CRYPT M Z N)
(REMAINDER (EXP M Z) N))
(NOT (EQUAL N 1))
(NUMBERP M))
(EQUAL
(REMAINDER (TIMES M
(TIMES (CRYPT M Z N) (CRYPT M Z N)))
N)
(REMAINDER (TIMES (EXP M Z) (TIMES (EXP M Z) M))
N))).
But this again simplifies, rewriting with
COMMUTATIVITY-OF-TIMES and COMMUTATIVITY2-OF-TIMES, to:
(IMPLIES
(AND (NUMBERP Z)
(EQUAL (CRYPT M Z N)
(REMAINDER (EXP M Z) N))
(NOT (EQUAL N 1))
(NUMBERP M))
(EQUAL
(REMAINDER (TIMES M
(TIMES (CRYPT M Z N) (CRYPT M Z N)))
N)
(REMAINDER (TIMES M (TIMES (EXP M Z) (EXP M Z)))
N))).
We now use the above equality hypothesis by substituting
(REMAINDER (EXP M Z) N) for (CRYPT M Z N) and throwing away the
equality. This produces:
(IMPLIES
(AND (NUMBERP Z)
(NOT (EQUAL N 1))
(NUMBERP M))
(EQUAL (REMAINDER (TIMES M
(TIMES (REMAINDER (EXP M Z) N)
(REMAINDER (EXP M Z) N)))
N)
(REMAINDER (TIMES M (TIMES (EXP M Z) (EXP M Z)))
N))),
which finally simplifies, appealing to the lemmas
COMMUTATIVITY-OF-TIMES and TIMES-MOD-2, to:
T.
So next consider:
(IMPLIES (AND (NUMBERP X)
(LESSP X N)
(NUMBERP V)
(NUMBERP N)
(NOT (EQUAL N 0))
(NOT (EQUAL N 1))
(NOT (NUMBERP M)))
(EQUAL (TIMES M (TIMES X X))
(TIMES 0
(TIMES N (TIMES N (TIMES V V)))))),
named *1.1 above. Perhaps we can prove it by induction. The
recursive terms in the conjecture suggest two inductions. However,
they merge into one likely candidate induction. We will induct
according to the following scheme:
(AND (IMPLIES (OR (EQUAL N 0) (NOT (NUMBERP N)))
(P M X N V))
(IMPLIES (AND (NOT (OR (EQUAL N 0) (NOT (NUMBERP N))))
(OR (EQUAL X 0) (NOT (NUMBERP X))))
(P M X N V))
(IMPLIES (AND (NOT (OR (EQUAL N 0) (NOT (NUMBERP N))))
(NOT (OR (EQUAL X 0) (NOT (NUMBERP X))))
(P M (SUB1 X) (SUB1 N) V))
(P M X N V))).
Linear arithmetic, the lemmas SUB1-LESSEQP and SUB1-LESSP, and the
definitions of OR and NOT inform us that the measure (COUNT X)
decreases according to the well-founded relation LESSP in each
induction step of the scheme. Note, however, the inductive instance
chosen for N. The above induction scheme leads to six new formulas:
Case 6. (IMPLIES (AND (OR (EQUAL N 0) (NOT (NUMBERP N)))
(NUMBERP X)
(LESSP X N)
(NUMBERP V)
(NUMBERP N)
(NOT (EQUAL N 0))
(NOT (EQUAL N 1))
(NOT (NUMBERP M)))
(EQUAL (TIMES M (TIMES X X))
(TIMES 0
(TIMES N (TIMES N (TIMES V V)))))).
This simplifies, expanding the definitions of NOT and OR, to:
T.
Case 5. (IMPLIES (AND (NOT (OR (EQUAL N 0) (NOT (NUMBERP N))))
(OR (EQUAL X 0) (NOT (NUMBERP X)))
(NUMBERP X)
(LESSP X N)
(NUMBERP V)
(NUMBERP N)
(NOT (EQUAL N 0))
(NOT (EQUAL N 1))
(NOT (NUMBERP M)))
(EQUAL (TIMES M (TIMES X X))
(TIMES 0
(TIMES N (TIMES N (TIMES V V)))))).
This simplifies, appealing to the lemmas TIMES-ZERO2,
COMMUTATIVITY-OF-TIMES, and TIMES-IDENTITY, and unfolding NOT, OR,
NUMBERP, EQUAL, LESSP, and TIMES, to:
T.
Case 4. (IMPLIES (AND (NOT (OR (EQUAL N 0) (NOT (NUMBERP N))))
(NOT (OR (EQUAL X 0) (NOT (NUMBERP X))))
( LEQ (SUB1 N) (SUB1 X))
(NUMBERP X)
(LESSP X N)
(NUMBERP V)
(NUMBERP N)
(NOT (EQUAL N 0))
(NOT (EQUAL N 1))
(NOT (NUMBERP M)))
(EQUAL (TIMES M (TIMES X X))
(TIMES 0
(TIMES N (TIMES N (TIMES V V)))))).
This simplifies, using linear arithmetic, to:
(IMPLIES (AND (EQUAL X 0)
(NOT (OR (EQUAL N 0) (NOT (NUMBERP N))))
(NOT (OR (EQUAL X 0) (NOT (NUMBERP X))))
( LEQ (SUB1 N) (SUB1 X))
(NUMBERP X)
(LESSP X N)
(NUMBERP V)
(NUMBERP N)
(NOT (EQUAL N 0))
(NOT (EQUAL N 1))
(NOT (NUMBERP M)))
(EQUAL (TIMES M (TIMES X X))
(TIMES 0
(TIMES N (TIMES N (TIMES V V)))))).
This again simplifies, opening up the functions NOT, OR, EQUAL, and
NUMBERP, to:
T.
Case 3. (IMPLIES (AND (NOT (OR (EQUAL N 0) (NOT (NUMBERP N))))
(NOT (OR (EQUAL X 0) (NOT (NUMBERP X))))
(EQUAL (SUB1 N) 0)
(NUMBERP X)
(LESSP X N)
(NUMBERP V)
(NUMBERP N)
(NOT (EQUAL N 0))
(NOT (EQUAL N 1))
(NOT (NUMBERP M)))
(EQUAL (TIMES M (TIMES X X))
(TIMES 0
(TIMES N (TIMES N (TIMES V V)))))),
which we simplify, using linear arithmetic, to:
T.
Case 2. (IMPLIES (AND (NOT (OR (EQUAL N 0) (NOT (NUMBERP N))))
(NOT (OR (EQUAL X 0) (NOT (NUMBERP X))))
(EQUAL (SUB1 N) 1)
(NUMBERP X)
(LESSP X N)
(NUMBERP V)
(NUMBERP N)
(NOT (EQUAL N 0))
(NOT (EQUAL N 1))
(NOT (NUMBERP M)))
(EQUAL (TIMES M (TIMES X X))
(TIMES 0
(TIMES N (TIMES N (TIMES V V)))))).
This simplifies, expanding NOT, OR, and LESSP, to:
(IMPLIES (AND (NOT (EQUAL X 0))
(EQUAL (SUB1 N) 1)
(NUMBERP X)
(LESSP (SUB1 X) (SUB1 N))
(NUMBERP V)
(NUMBERP N)
(NOT (EQUAL N 0))
(NOT (EQUAL N 1))
(NOT (NUMBERP M)))
(EQUAL (TIMES M (TIMES X X))
(TIMES 0
(TIMES N (TIMES N (TIMES V V)))))),
which we again simplify, using linear arithmetic, to:
(IMPLIES (AND (NOT (EQUAL 1 0))
(EQUAL (SUB1 N) 1)
(NUMBERP 1)
(LESSP (SUB1 1) 1)
(NUMBERP V)
(NUMBERP N)
(NOT (EQUAL N 0))
(NOT (EQUAL N 1))
(NOT (NUMBERP M)))
(EQUAL (TIMES M (TIMES 1 1))
(TIMES 0
(TIMES N (TIMES N (TIMES V V)))))),
which again simplifies, applying TIMES-1, COMMUTATIVITY-OF-TIMES,
and TIMES-IDENTITY, and opening up the functions EQUAL, NUMBERP,
SUB1, LESSP, and TIMES, to:
T.
Case 1. (IMPLIES
(AND (NOT (OR (EQUAL N 0) (NOT (NUMBERP N))))
(NOT (OR (EQUAL X 0) (NOT (NUMBERP X))))
(EQUAL (TIMES M (TIMES (SUB1 X) (SUB1 X)))
(TIMES 0
(TIMES (SUB1 N)
(TIMES (SUB1 N) (TIMES V V)))))
(NUMBERP X)
(LESSP X N)
(NUMBERP V)
(NUMBERP N)
(NOT (EQUAL N 0))
(NOT (EQUAL N 1))
(NOT (NUMBERP M)))
(EQUAL (TIMES M (TIMES X X))
(TIMES 0
(TIMES N (TIMES N (TIMES V V)))))).
This simplifies, applying COMMUTATIVITY-OF-TIMES and
COMMUTATIVITY2-OF-TIMES, and opening up the definitions of NOT, OR,
and LESSP, to:
(IMPLIES
(AND
(NOT (EQUAL X 0))
(EQUAL (TIMES M (TIMES (SUB1 X) (SUB1 X)))
(TIMES 0
(TIMES V
(TIMES V (TIMES (SUB1 N) (SUB1 N))))))
(NUMBERP X)
(LESSP (SUB1 X) (SUB1 N))
(NUMBERP V)
(NUMBERP N)
(NOT (EQUAL N 0))
(NOT (EQUAL N 1))
(NOT (NUMBERP M)))
(EQUAL (TIMES M (TIMES X X))
(TIMES 0
(TIMES N (TIMES N (TIMES V V)))))).
Applying the lemma SUB1-ELIM, replace X by (ADD1 Z) to eliminate
(SUB1 X). We employ the type restriction lemma noted when SUB1 was
introduced to constrain the new variable. We must thus prove:
(IMPLIES
(AND
(NUMBERP Z)
(NOT (EQUAL (ADD1 Z) 0))
(EQUAL (TIMES M (TIMES Z Z))
(TIMES 0
(TIMES V
(TIMES V (TIMES (SUB1 N) (SUB1 N))))))
(LESSP Z (SUB1 N))
(NUMBERP V)
(NUMBERP N)
(NOT (EQUAL N 0))
(NOT (EQUAL N 1))
(NOT (NUMBERP M)))
(EQUAL (TIMES M (TIMES (ADD1 Z) (ADD1 Z)))
(TIMES 0
(TIMES N (TIMES N (TIMES V V)))))),
which further simplifies, applying TIMES-ADD1,
COMMUTATIVITY-OF-TIMES, SUB1-ADD1, PLUS-ADD1,
COMMUTATIVITY2-OF-PLUS, EQUAL-TIMES-0, and
DISTRIBUTIVITY-OF-TIMES-OVER-PLUS, and opening up the definition of
PLUS, to:
(IMPLIES
(AND
(NUMBERP Z)
(EQUAL (TIMES M (TIMES Z Z))
(TIMES 0
(TIMES V
(TIMES V (TIMES (SUB1 N) (SUB1 N))))))
(LESSP Z (SUB1 N))
(NUMBERP V)
(NUMBERP N)
(NOT (EQUAL N 0))
(NOT (EQUAL N 1))
(NOT (NUMBERP M)))
(EQUAL (TIMES M (TIMES Z Z))
(TIMES 0
(TIMES N (TIMES N (TIMES V V)))))),
which again simplifies, using linear arithmetic, to:
T.
That finishes the proof of *1.1, which, in turn, finishes the
proof of *1. Q.E.D.
[ 167.185993 3.4860077 ]
CRYPT-CORRECT
(PROVE-LEMMA TIMES-MOD-3
(REWRITE)
(EQUAL (REMAINDER (TIMES (REMAINDER A N) B)
N)
(REMAINDER (TIMES A B) N)))
This formula simplifies, applying COMMUTATIVITY-OF-TIMES and
TIMES-MOD-1, to:
T.
Q.E.D.
[ 1.22899984 0.0150004069 ]
TIMES-MOD-3
(PROVE-LEMMA REMAINDER-EXP-LEMMA
(REWRITE)
(IMPLIES (EQUAL (REMAINDER Y A)
(REMAINDER Z A))
(EQUAL (EQUAL (REMAINDER (TIMES X Y) A)
(REMAINDER (TIMES X Z) A))
T)))
.
Applying the lemma REMAINDER-QUOTIENT-ELIM, we now replace Y by
(PLUS V (TIMES A W)) to eliminate (REMAINDER Y A) and (QUOTIENT Y A).
We rely upon LESSP-REMAINDER2, the type restriction lemma noted when
REMAINDER was introduced, and the type restriction lemma noted when
QUOTIENT was introduced to constrain the new variables. This
generates four new conjectures:
Case 4. (IMPLIES (AND (NOT (NUMBERP Y))
(EQUAL (REMAINDER Y A)
(REMAINDER Z A)))
(EQUAL (REMAINDER (TIMES X Y) A)
(REMAINDER (TIMES X Z) A))).
However this simplifies further, applying the lemmas TIMES-ZERO2
and REMAINDER-0-CROCK, and expanding the definitions of LESSP and
REMAINDER, to the formula:
(IMPLIES (AND (NOT (NUMBERP Y))
(EQUAL 0 (REMAINDER Z A)))
(EQUAL 0 (REMAINDER (TIMES X Z) A))).
Applying the lemma REMAINDER-QUOTIENT-ELIM, replace Z by
(PLUS V (TIMES A W)) to eliminate (REMAINDER Z A) and
(QUOTIENT Z A). We employ LESSP-REMAINDER2, the type restriction
lemma noted when REMAINDER was introduced, and the type restriction
lemma noted when QUOTIENT was introduced to restrict the new
variables. This generates the following four new formulas:
Case 4.4.
(IMPLIES (AND (NOT (NUMBERP Z))
(NOT (NUMBERP Y))
(EQUAL 0 (REMAINDER Z A)))
(EQUAL 0 (REMAINDER (TIMES X Z) A))).
However this simplifies further, rewriting with TIMES-ZERO2 and
REMAINDER-0-CROCK, and opening up LESSP, REMAINDER, and EQUAL, to:
T.
Case 4.3.
(IMPLIES (AND (EQUAL A 0)
(NOT (NUMBERP Y))
(EQUAL 0 (REMAINDER Z A)))
(EQUAL 0 (REMAINDER (TIMES X Z) A))),
which further simplifies, applying COMMUTATIVITY-OF-TIMES,
REMAINDER-TIMES, and TIMES-ZERO2, and expanding the functions
EQUAL and REMAINDER, to:
T.
Case 4.2.
(IMPLIES (AND (NOT (NUMBERP A))
(NOT (NUMBERP Y))
(EQUAL 0 (REMAINDER Z A)))
(EQUAL 0 (REMAINDER (TIMES X Z) A))),
which we further simplify, rewriting with REMAINDER-WRT-12,
COMMUTATIVITY-OF-TIMES, TIMES-IDENTITY, TIMES-ZERO2, and
REMAINDER-0-CROCK, and expanding the definition of EQUAL, to:
T.
Case 4.1.
(IMPLIES (AND (NUMBERP V)
(EQUAL (LESSP V A) (NOT (ZEROP A)))
(NUMBERP W)
(NUMBERP A)
(NOT (EQUAL A 0))
(NOT (NUMBERP Y))
(EQUAL 0 V))
(EQUAL 0
(REMAINDER (TIMES X (PLUS V (TIMES A W)))
A))),
which we further simplify, applying COMMUTATIVITY-OF-TIMES,
COMMUTATIVITY2-OF-TIMES, and REMAINDER-TIMES, and opening up
NUMBERP, EQUAL, LESSP, ZEROP, NOT, and PLUS, to:
T.
Case 3. (IMPLIES (AND (EQUAL A 0)
(EQUAL (REMAINDER Y A)
(REMAINDER Z A)))
(EQUAL (REMAINDER (TIMES X Y) A)
(REMAINDER (TIMES X Z) A))).
But this simplifies further, rewriting with TIMES-ZERO2,
COMMUTATIVITY-OF-TIMES, and REMAINDER-TIMES, and expanding the
functions EQUAL and REMAINDER, to:
T.
Case 2. (IMPLIES (AND (NOT (NUMBERP A))
(EQUAL (REMAINDER Y A)
(REMAINDER Z A)))
(EQUAL (REMAINDER (TIMES X Y) A)
(REMAINDER (TIMES X Z) A))).
However this simplifies further, rewriting with the lemmas
REMAINDER-WRT-12, TIMES-ZERO2, REMAINDER-0-CROCK,
COMMUTATIVITY-OF-TIMES, and TIMES-IDENTITY, and expanding the
definition of EQUAL, to:
T.
Case 1. (IMPLIES (AND (NUMBERP V)
(EQUAL (LESSP V A) (NOT (ZEROP A)))
(NUMBERP W)
(NUMBERP A)
(NOT (EQUAL A 0))
(EQUAL V (REMAINDER Z A)))
(EQUAL (REMAINDER (TIMES X (PLUS V (TIMES A W)))
A)
(REMAINDER (TIMES X Z) A))).
However this further simplifies, applying LESSP-REMAINDER2,
COMMUTATIVITY-OF-TIMES, COMMUTATIVITY2-OF-TIMES,
COMMUTATIVITY-OF-PLUS, and DISTRIBUTIVITY-OF-TIMES-OVER-PLUS, and
opening up the definitions of ZEROP, NOT, and EQUAL, to the new
formula:
(IMPLIES (AND (NUMBERP W)
(NUMBERP A)
(NOT (EQUAL A 0)))
(EQUAL (REMAINDER (PLUS (TIMES A (TIMES W X))
(TIMES X (REMAINDER Z A)))
A)
(REMAINDER (TIMES X Z) A))).
Applying the lemma REMAINDER-QUOTIENT-ELIM, we now replace Z by
(PLUS V (TIMES A D)) to eliminate (REMAINDER Z A) and
(QUOTIENT Z A). We use LESSP-REMAINDER2, the type restriction
lemma noted when REMAINDER was introduced, and the type restriction
lemma noted when QUOTIENT was introduced to restrict the new
variables. We thus obtain two new conjectures:
Case 1.2.
(IMPLIES (AND (NOT (NUMBERP Z))
(NUMBERP W)
(NUMBERP A)
(NOT (EQUAL A 0)))
(EQUAL (REMAINDER (PLUS (TIMES A (TIMES W X))
(TIMES X (REMAINDER Z A)))
A)
(REMAINDER (TIMES X Z) A))),
which we further simplify, appealing to the lemmas
COMMUTATIVITY-OF-TIMES, TIMES-IDENTITY, COMMUTATIVITY-OF-PLUS,
REMAINDER-TIMES, TIMES-ZERO2, and REMAINDER-0-CROCK, and
expanding the functions LESSP, REMAINDER, EQUAL, and PLUS, to:
T.
Case 1.1.
(IMPLIES (AND (NUMBERP V)
(EQUAL (LESSP V A) (NOT (ZEROP A)))
(NUMBERP D)
(NUMBERP W)
(NUMBERP A)
(NOT (EQUAL A 0)))
(EQUAL (REMAINDER (PLUS (TIMES A (TIMES W X))
(TIMES X V))
A)
(REMAINDER (TIMES X (PLUS V (TIMES A D)))
A))),
which we further simplify, rewriting with COMMUTATIVITY-OF-TIMES,
COMMUTATIVITY-OF-PLUS, REMAINDER-PLUS-TIMES-2,
COMMUTATIVITY2-OF-TIMES, and DISTRIBUTIVITY-OF-TIMES-OVER-PLUS,
and opening up the functions ZEROP and NOT, to:
T.
Q.E.D.
[ 43.924011 0.72298584 ]
REMAINDER-EXP-LEMMA
(PROVE-LEMMA REMAINDER-EXP
(REWRITE)
(EQUAL (REMAINDER (EXP (REMAINDER A N) I) N)
(REMAINDER (EXP A I) N)))
.
Appealing to the lemma REMAINDER-QUOTIENT-ELIM, we now replace A by
(PLUS X (TIMES N Z)) to eliminate (REMAINDER A N) and (QUOTIENT A N).
We rely upon LESSP-REMAINDER2, the type restriction lemma noted when
REMAINDER was introduced, and the type restriction lemma noted when
QUOTIENT was introduced to restrict the new variables. This produces
the following four new goals:
Case 4. (IMPLIES (NOT (NUMBERP A))
(EQUAL (REMAINDER (EXP (REMAINDER A N) I) N)
(REMAINDER (EXP A I) N))),
which simplifies, rewriting with EXP-OF-0, and expanding the
functions LESSP and REMAINDER, to three new conjectures:
Case 4.3.
(IMPLIES (AND (NOT (NUMBERP A))
(NOT (EQUAL I 0))
(NUMBERP I))
(EQUAL (REMAINDER 0 N)
(REMAINDER (EXP A I) N))),
which we again simplify, rewriting with REMAINDER-0-CROCK, to:
(IMPLIES (AND (NOT (NUMBERP A))
(NOT (EQUAL I 0))
(NUMBERP I))
(EQUAL 0 (REMAINDER (EXP A I) N))),
which we would normally push and work on later by induction. But
if we must use induction to prove the input conjecture, we prefer
to induct on the original formulation of the problem. Thus we
will disregard all that we have previously done, give the name *1
to the original input, and work on it.
So now let us return to:
(EQUAL (REMAINDER (EXP (REMAINDER A N) I) N)
(REMAINDER (EXP A I) N)).
We named this *1. We will appeal to induction. There are three
plausible inductions. They merge into two likely candidate
inductions. However, only one is unflawed. We will induct according
to the following scheme:
(AND (IMPLIES (ZEROP I) (P A N I))
(IMPLIES (AND (NOT (ZEROP I)) (P A N (SUB1 I)))
(P A N I))).
Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of
ZEROP can be used to show that the measure (COUNT I) decreases
according to the well-founded relation LESSP in each induction step
of the scheme. The above induction scheme leads to two new formulas:
Case 2. (IMPLIES (ZEROP I)
(EQUAL (REMAINDER (EXP (REMAINDER A N) I) N)
(REMAINDER (EXP A I) N))),
which we simplify, applying EXP-BY-0 and REMAINDER-OF-1, and
expanding the definitions of ZEROP and EXP, to:
T.
Case 1. (IMPLIES (AND (NOT (ZEROP I))
(EQUAL (REMAINDER (EXP (REMAINDER A N) (SUB1 I))
N)
(REMAINDER (EXP A (SUB1 I)) N)))
(EQUAL (REMAINDER (EXP (REMAINDER A N) I) N)
(REMAINDER (EXP A I) N))),
which we simplify, rewriting with TIMES-MOD-3 and
REMAINDER-EXP-LEMMA, and unfolding ZEROP and EXP, to:
T.
That finishes the proof of *1. Q.E.D.
[ 7.3329956 0.351005044 ]
REMAINDER-EXP
(PROVE-LEMMA EXP-MOD-IS-1
(REWRITE)
(IMPLIES (EQUAL (REMAINDER (EXP M J) P) 1.)
(EQUAL (REMAINDER (EXP M (TIMES I J)) P)
1.))
((USE (EXP-EXP (I M) (J J) (K I))
(REMAINDER-EXP (A (EXP M J)) (N P)))
(DISABLE EXP-EXP REMAINDER-EXP)))
This simplifies, applying the lemmas COMMUTATIVITY-OF-TIMES, EXP-OF-1,
REMAINDER-OF-1, and REMAINDER-WRT-1, and expanding the definition of
EQUAL, to:
T.
Q.E.D.
[ 1.36600342 0.056994629 ]
EXP-MOD-IS-1
(DEFN PDIFFERENCE
(A B)
(IF (LESSP A B)
(DIFFERENCE B A)
(DIFFERENCE A B))
NIL)
Observe that (NUMBERP (PDIFFERENCE A B)) is a theorem.
[ 0.73099772 0.0109985352 ]
PDIFFERENCE
(PROVE-LEMMA TIMES-DISTRIBUTES-OVER-PDIFFERENCE
(REWRITE)
(EQUAL (TIMES M (PDIFFERENCE A B))
(PDIFFERENCE (TIMES M A)
(TIMES M B))))
This formula simplifies, applying COMMUTATIVITY-OF-TIMES and
LESSP-TIMES-CANCELLATION, and expanding the definition of PDIFFERENCE,
to four new goals:
Case 4. (IMPLIES ( LEQ B A)
(EQUAL (TIMES M (DIFFERENCE A B))
(DIFFERENCE (TIMES A M)
(TIMES B M)))),
which we again simplify, rewriting with TIMES-DIFFERENCE, to:
T.
Case 3. (IMPLIES (AND (NOT (NUMBERP M)) (LESSP A B))
(EQUAL (TIMES M (DIFFERENCE B A))
(DIFFERENCE (TIMES A M)
(TIMES B M)))).
This again simplifies, applying TIMES-ZERO2 and TIMES-DIFFERENCE,
and expanding the definitions of DIFFERENCE and EQUAL, to:
T.
Case 2. (IMPLIES (AND (EQUAL M 0) (LESSP A B))
(EQUAL (TIMES M (DIFFERENCE B A))
(DIFFERENCE (TIMES A M)
(TIMES B M)))),
which again simplifies, using linear arithmetic, rewriting with
COMMUTATIVITY-OF-TIMES, DIFFERENCE-0, and TIMES-DIFFERENCE, and
opening up EQUAL, to:
T.
Case 1. (IMPLIES (AND (NOT (EQUAL M 0))
(NUMBERP M)
(LESSP A B))
(EQUAL (TIMES M (DIFFERENCE B A))
(DIFFERENCE (TIMES B M)
(TIMES A M)))),
which again simplifies, appealing to the lemma TIMES-DIFFERENCE, to:
T.
Q.E.D.
[ 5.1459961 0.25300293 ]
TIMES-DISTRIBUTES-OVER-PDIFFERENCE
(PROVE-LEMMA EQUAL-MODS-TRICK-1
(REWRITE)
(IMPLIES (EQUAL (REMAINDER (PDIFFERENCE A B) P)
0.)
(EQUAL (EQUAL (REMAINDER A P)
(REMAINDER B P))
T)))
This formula simplifies, expanding the function PDIFFERENCE, to two
new formulas:
Case 2. (IMPLIES (AND ( LEQ B A)
(EQUAL (REMAINDER (DIFFERENCE A B) P)
0))
(EQUAL (REMAINDER A P)
(REMAINDER B P))).
Appealing to the lemmas DIFFERENCE-ELIM and REMAINDER-QUOTIENT-ELIM,
we now replace A by (PLUS B X) to eliminate (DIFFERENCE A B) and X
by (PLUS Z (TIMES P V)) to eliminate (REMAINDER X P) and
(QUOTIENT X P). We rely upon the type restriction lemma noted when
DIFFERENCE was introduced, LESSP-REMAINDER2, the type restriction
lemma noted when REMAINDER was introduced, and the type restriction
lemma noted when QUOTIENT was introduced to restrict the new
variables. This produces the following four new goals:
Case 2.4.
(IMPLIES (AND (NOT (NUMBERP A))
( LEQ B A)
(EQUAL (REMAINDER (DIFFERENCE A B) P)
0))
(EQUAL (REMAINDER A P)
(REMAINDER B P))),
which further simplifies, using linear arithmetic, rewriting with
DIFFERENCE-0 and REMAINDER-0-CROCK, and expanding the functions
LESSP, EQUAL, and REMAINDER, to:
T.
Case 2.3.
(IMPLIES (AND (EQUAL P 0)
(NUMBERP X)
( LEQ B (PLUS B X))
(EQUAL (REMAINDER X P) 0))
(EQUAL (REMAINDER (PLUS B X) P)
(REMAINDER B P))),
which we further simplify, applying COMMUTATIVITY-OF-PLUS, and
opening up EQUAL, REMAINDER, and PLUS, to:
T.
Case 2.2.
(IMPLIES (AND (NOT (NUMBERP P))
(NUMBERP X)
( LEQ B (PLUS B X))
(EQUAL (REMAINDER X P) 0))
(EQUAL (REMAINDER (PLUS B X) P)
(REMAINDER B P))),
which we further simplify, rewriting with REMAINDER-WRT-12 and
COMMUTATIVITY-OF-PLUS, and unfolding the functions EQUAL and PLUS,
to:
T.
Case 2.1.
(IMPLIES (AND (NUMBERP Z)
(EQUAL (LESSP Z P) (NOT (ZEROP P)))
(NUMBERP V)
(NUMBERP P)
(NOT (EQUAL P 0))
( LEQ B (PLUS B (PLUS Z (TIMES P V))))
(EQUAL Z 0))
(EQUAL (REMAINDER (PLUS B (PLUS Z (TIMES P V)))
P)
(REMAINDER B P))).
But this simplifies further, applying REMAINDER-PLUS-TIMES-2, and
unfolding the definitions of NUMBERP, EQUAL, LESSP, ZEROP, NOT,
and PLUS, to:
T.
Case 1. (IMPLIES (AND (LESSP A B)
(EQUAL (REMAINDER (DIFFERENCE B A) P)
0))
(EQUAL (REMAINDER A P)
(REMAINDER B P))).
Applying the lemmas DIFFERENCE-ELIM and REMAINDER-QUOTIENT-ELIM, we
now replace B by (PLUS A X) to eliminate (DIFFERENCE B A) and X by
(PLUS Z (TIMES P V)) to eliminate (REMAINDER X P) and
(QUOTIENT X P). We employ the type restriction lemma noted when
DIFFERENCE was introduced, LESSP-REMAINDER2, the type restriction
lemma noted when REMAINDER was introduced, and the type restriction
lemma noted when QUOTIENT was introduced to constrain the new
variables. The result is five new conjectures:
Case 1.5.
(IMPLIES (AND (LESSP B A)
(LESSP A B)
(EQUAL (REMAINDER (DIFFERENCE B A) P)
0))
(EQUAL (REMAINDER A P)
(REMAINDER B P))),
which we further simplify, using linear arithmetic, to:
T.
Case 1.4.
(IMPLIES (AND (NOT (NUMBERP B))
(LESSP A B)
(EQUAL (REMAINDER (DIFFERENCE B A) P)
0))
(EQUAL (REMAINDER A P)
(REMAINDER B P))),
which further simplifies, expanding the definition of LESSP, to:
T.
Case 1.3.
(IMPLIES (AND (EQUAL P 0)
(NUMBERP X)
( LEQ A (PLUS A X))
(LESSP A (PLUS A X))
(EQUAL (REMAINDER X P) 0))
(EQUAL (REMAINDER A P)
(REMAINDER (PLUS A X) P))),
which we further simplify, applying COMMUTATIVITY-OF-PLUS, and
opening up EQUAL, REMAINDER, and PLUS, to:
T.
Case 1.2.
(IMPLIES (AND (NOT (NUMBERP P))
(NUMBERP X)
( LEQ A (PLUS A X))
(LESSP A (PLUS A X))
(EQUAL (REMAINDER X P) 0))
(EQUAL (REMAINDER A P)
(REMAINDER (PLUS A X) P))).
But this simplifies further, rewriting with REMAINDER-WRT-12 and
COMMUTATIVITY-OF-PLUS, and expanding the functions EQUAL and PLUS,
to:
T.
Case 1.1.
(IMPLIES (AND (NUMBERP Z)
(EQUAL (LESSP Z P) (NOT (ZEROP P)))
(NUMBERP V)
(NUMBERP P)
(NOT (EQUAL P 0))
( LEQ A (PLUS A (PLUS Z (TIMES P V))))
(LESSP A
(PLUS A (PLUS Z (TIMES P V))))
(EQUAL Z 0))
(EQUAL (REMAINDER A P)
(REMAINDER (PLUS A (PLUS Z (TIMES P V)))
P))).
However this simplifies further, rewriting with the lemma
REMAINDER-PLUS-TIMES-2, and expanding the definitions of NUMBERP,
EQUAL, LESSP, ZEROP, NOT, and PLUS, to:
T.
Q.E.D.
[ 19.2679892 0.52600911 ]
EQUAL-MODS-TRICK-1
(PROVE-LEMMA EQUAL-MODS-TRICK-2
(REWRITE)
(IMPLIES (EQUAL (REMAINDER A P)
(REMAINDER B P))
(EQUAL (REMAINDER (PDIFFERENCE A B) P)
0.))
((DISABLE DIFFERENCE-ELIM)))
This conjecture simplifies, unfolding the function PDIFFERENCE, to
two new conjectures:
Case 2. (IMPLIES (AND (EQUAL (REMAINDER A P)
(REMAINDER B P))
( LEQ B A))
(EQUAL (REMAINDER (DIFFERENCE A B) P)
0)).
Appealing to the lemma REMAINDER-QUOTIENT-ELIM, replace A by
(PLUS X (TIMES P Z)) to eliminate (REMAINDER A P) and
(QUOTIENT A P). We rely upon LESSP-REMAINDER2, the type
restriction lemma noted when REMAINDER was introduced, and the type
restriction lemma noted when QUOTIENT was introduced to restrict
the new variables. We would thus like to prove four new
conjectures:
Case 2.4.
(IMPLIES (AND (NOT (NUMBERP A))
(EQUAL (REMAINDER A P)
(REMAINDER B P))
( LEQ B A))
(EQUAL (REMAINDER (DIFFERENCE A B) P)
0)),
which further simplifies, using linear arithmetic, rewriting with
DIFFERENCE-0 and REMAINDER-0-CROCK, and opening up LESSP,
REMAINDER, and EQUAL, to:
T.
Case 2.3.
(IMPLIES (AND (EQUAL P 0)
(EQUAL (REMAINDER A P)
(REMAINDER B P))
( LEQ B A))
(EQUAL (REMAINDER (DIFFERENCE A B) P)
0)),
which further simplifies, using linear arithmetic, appealing to
the lemma DIFFERENCE-0, and unfolding the definitions of EQUAL,
REMAINDER, and LESSP, to:
T.
Case 2.2.
(IMPLIES (AND (NOT (NUMBERP P))
(EQUAL (REMAINDER A P)
(REMAINDER B P))
( LEQ B A))
(EQUAL (REMAINDER (DIFFERENCE A B) P)
0)),
which we further simplify, using linear arithmetic, rewriting
with REMAINDER-WRT-12, DIFFERENCE-0, and REMAINDER-0-CROCK, and
opening up EQUAL and LESSP, to:
T.
Case 2.1.
(IMPLIES
(AND (NUMBERP X)
(EQUAL (LESSP X P) (NOT (ZEROP P)))
(NUMBERP Z)
(NUMBERP P)
(NOT (EQUAL P 0))
(EQUAL X (REMAINDER B P))
( LEQ B (PLUS X (TIMES P Z))))
(EQUAL (REMAINDER (DIFFERENCE (PLUS X (TIMES P Z)) B)
P)
0)),
which further simplifies, applying LESSP-REMAINDER2, and
expanding the functions ZEROP, NOT, and EQUAL, to:
(IMPLIES
(AND (NUMBERP Z)
(NUMBERP P)
(NOT (EQUAL P 0))
( LEQ B
(PLUS (REMAINDER B P) (TIMES P Z))))
(EQUAL
(REMAINDER (DIFFERENCE (PLUS (REMAINDER B P) (TIMES P Z))
B)
P)
0)).
Applying the lemma REMAINDER-QUOTIENT-ELIM, replace B by
(PLUS X (TIMES P V)) to eliminate (REMAINDER B P) and
(QUOTIENT B P). We rely upon LESSP-REMAINDER2, the type
restriction lemma noted when REMAINDER was introduced, and the
type restriction lemma noted when QUOTIENT was introduced to
restrict the new variables. This produces two new conjectures:
Case 2.1.2.
(IMPLIES
(AND (NOT (NUMBERP B))
(NUMBERP Z)
(NUMBERP P)
(NOT (EQUAL P 0))
( LEQ B
(PLUS (REMAINDER B P) (TIMES P Z))))
(EQUAL
(REMAINDER
(DIFFERENCE (PLUS (REMAINDER B P) (TIMES P Z))
B)
P)
0)).
However this further simplifies, rewriting with the lemma
EQUAL-TIMES-0, and unfolding the definitions of LESSP,
REMAINDER, EQUAL, PLUS, and DIFFERENCE, to two new conjectures:
Case 2.1.2.2.
(IMPLIES (AND (NOT (NUMBERP B))
(NUMBERP Z)
(NUMBERP P)
(NOT (EQUAL P 0))
(NOT (EQUAL Z 0)))
(EQUAL (REMAINDER (TIMES P Z) P) 0)),
which we finally simplify, rewriting with the lemma
REMAINDER-TIMES, and expanding the definition of EQUAL, to:
T.
Case 2.1.2.1.
(IMPLIES (AND (NOT (NUMBERP B))
(NUMBERP Z)
(NUMBERP P)
(NOT (EQUAL P 0))
(EQUAL Z 0))
(EQUAL (REMAINDER 0 P) 0)).
However this finally simplifies, applying REMAINDER-0-CROCK,
and opening up the definitions of NUMBERP and EQUAL, to:
T.
Case 2.1.1.
(IMPLIES
(AND (NUMBERP X)
(EQUAL (LESSP X P) (NOT (ZEROP P)))
(NUMBERP V)
(NUMBERP Z)
(NUMBERP P)
(NOT (EQUAL P 0))
( LEQ
(PLUS X (TIMES P V))
(PLUS X (TIMES P Z))))
(EQUAL (REMAINDER (DIFFERENCE (PLUS X (TIMES P Z))
(PLUS X (TIMES P V)))
P)
0)).
But this further simplifies, applying LESSP-PLUS-CANCELATION,
DIFFERENCE-PLUS-CANCELATION, and REMAINDER-DIFFERENCE-TIMES,
and opening up the functions ZEROP, NOT, and EQUAL, to:
T.
Case 1. (IMPLIES (AND (EQUAL (REMAINDER A P)
(REMAINDER B P))
(LESSP A B))
(EQUAL (REMAINDER (DIFFERENCE B A) P)
0)).
Appealing to the lemma REMAINDER-QUOTIENT-ELIM, we now replace A by
(PLUS X (TIMES P Z)) to eliminate (REMAINDER A P) and
(QUOTIENT A P). We rely upon LESSP-REMAINDER2, the type
restriction lemma noted when REMAINDER was introduced, and the type
restriction lemma noted when QUOTIENT was introduced to constrain
the new variables. We thus obtain four new goals:
Case 1.4.
(IMPLIES (AND (NOT (NUMBERP A))
(EQUAL (REMAINDER A P)
(REMAINDER B P))
(LESSP A B))
(EQUAL (REMAINDER (DIFFERENCE B A) P)
0)),
which we further simplify, opening up the definitions of LESSP,
REMAINDER, DIFFERENCE, and EQUAL, to:
T.
Case 1.3.
(IMPLIES (AND (EQUAL P 0)
(EQUAL (REMAINDER A P)
(REMAINDER B P))
(LESSP A B))
(EQUAL (REMAINDER (DIFFERENCE B A) P)
0)),
which we further simplify, appealing to the lemma DIFFERENCE-X-X,
and unfolding the functions EQUAL, REMAINDER, and LESSP, to:
T.
Case 1.2.
(IMPLIES (AND (NOT (NUMBERP P))
(EQUAL (REMAINDER A P)
(REMAINDER B P))
(LESSP A B))
(EQUAL (REMAINDER (DIFFERENCE B A) P)
0)).
But this further simplifies, rewriting with the lemmas
REMAINDER-WRT-12, DIFFERENCE-X-X, and REMAINDER-0-CROCK, and
expanding the definitions of EQUAL and LESSP, to:
T.
Case 1.1.
(IMPLIES
(AND (NUMBERP X)
(EQUAL (LESSP X P) (NOT (ZEROP P)))
(NUMBERP Z)
(NUMBERP P)
(NOT (EQUAL P 0))
(EQUAL X (REMAINDER B P))
(LESSP (PLUS X (TIMES P Z)) B))
(EQUAL (REMAINDER (DIFFERENCE B (PLUS X (TIMES P Z)))
P)
0)).
This further simplifies, rewriting with the lemma
LESSP-REMAINDER2, and expanding the functions ZEROP, NOT, and
EQUAL, to:
(IMPLIES
(AND (NUMBERP Z)
(NUMBERP P)
(NOT (EQUAL P 0))
(LESSP (PLUS (REMAINDER B P) (TIMES P Z))
B))
(EQUAL
(REMAINDER (DIFFERENCE B
(PLUS (REMAINDER B P) (TIMES P Z)))
P)
0)).
Applying the lemma REMAINDER-QUOTIENT-ELIM, we now replace B by
(PLUS X (TIMES P V)) to eliminate (REMAINDER B P) and
(QUOTIENT B P). We rely upon LESSP-REMAINDER2, the type
restriction lemma noted when REMAINDER was introduced, and the
type restriction lemma noted when QUOTIENT was introduced to
restrict the new variables. This generates two new goals:
Case 1.1.2.
(IMPLIES
(AND (NOT (NUMBERP B))
(NUMBERP Z)
(NUMBERP P)
(NOT (EQUAL P 0))
(LESSP (PLUS (REMAINDER B P) (TIMES P Z))
B))
(EQUAL
(REMAINDER
(DIFFERENCE B
(PLUS (REMAINDER B P) (TIMES P Z)))
P)
0)),
which further simplifies, expanding LESSP, REMAINDER, EQUAL,
and PLUS, to:
T.
Case 1.1.1.
(IMPLIES
(AND (NUMBERP X)
(EQUAL (LESSP X P) (NOT (ZEROP P)))
(NUMBERP V)
(NUMBERP Z)
(NUMBERP P)
(NOT (EQUAL P 0))
(LESSP (PLUS X (TIMES P Z))
(PLUS X (TIMES P V))))
(EQUAL (REMAINDER (DIFFERENCE (PLUS X (TIMES P V))
(PLUS X (TIMES P Z)))
P)
0)).
This simplifies further, rewriting with the lemmas
LESSP-PLUS-CANCELATION, DIFFERENCE-PLUS-CANCELATION, and
REMAINDER-DIFFERENCE-TIMES, and expanding the functions ZEROP,
NOT, and EQUAL, to:
T.
Q.E.D.
[ 47.610014 0.96798503 ]
EQUAL-MODS-TRICK-2
(DISABLE PDIFFERENCE)
[ 6.99869794E-3 0.0 ]
G0006
(PROVE-LEMMA PRIME-KEY-TRICK
(REWRITE)
(IMPLIES (AND (EQUAL (REMAINDER (TIMES M A) P)
(REMAINDER (TIMES M B) P))
(NOT (EQUAL (REMAINDER M P) 0.))
(PRIME P))
(EQUAL (EQUAL (REMAINDER A P)
(REMAINDER B P))
T))
((USE (PRIME-KEY-REWRITE (A M)
(B (PDIFFERENCE A B)))
(EQUAL-MODS-TRICK-2 (A (TIMES M A))
(B (TIMES M B))))
(DISABLE PRIME-KEY-REWRITE EQUAL-MODS-TRICK-2)))
WARNING: Note that PRIME-KEY-TRICK contains the free variable M
which will be chosen by instantiating the hypothesis:
(EQUAL (REMAINDER (TIMES M A) P)
(REMAINDER (TIMES M B) P))
.
This formula can be simplified, using the abbreviations PRIME, NOT,
IMPLIES, and AND, to the new conjecture:
(IMPLIES
(AND
(IMPLIES (PRIME P)
(EQUAL (EQUAL (REMAINDER (TIMES M (PDIFFERENCE A B))
P)
0)
(OR (EQUAL (REMAINDER M P) 0)
(EQUAL (REMAINDER (PDIFFERENCE A B) P)
0))))
(IMPLIES
(EQUAL (REMAINDER (TIMES M A) P)
(REMAINDER (TIMES M B) P))
(EQUAL (REMAINDER (PDIFFERENCE (TIMES M A) (TIMES M B))
P)
0))
(EQUAL (REMAINDER (TIMES M A) P)
(REMAINDER (TIMES M B) P))
(NOT (EQUAL (REMAINDER M P) 0))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P)))
(EQUAL (EQUAL (REMAINDER A P)
(REMAINDER B P))
T)).
This simplifies, rewriting with COMMUTATIVITY-OF-TIMES,
TIMES-DISTRIBUTES-OVER-PDIFFERENCE, and EQUAL-MODS-TRICK-1, and
opening up the definitions of PRIME, OR, IMPLIES, and EQUAL, to:
T.
Q.E.D.
[ 20.7850058 0.097998047 ]
PRIME-KEY-TRICK
(PROVE-LEMMA PRODUCT-DIVIDES-LEMMA
(REWRITE)
(IMPLIES (EQUAL (REMAINDER X Z) 0.)
(EQUAL (REMAINDER (TIMES Y X) (TIMES Y Z))
0.)))
This conjecture simplifies, rewriting with COMMUTATIVITY-OF-TIMES, to
the new conjecture:
(IMPLIES (EQUAL (REMAINDER X Z) 0)
(EQUAL (REMAINDER (TIMES X Y) (TIMES Y Z))
0)).
Appealing to the lemma REMAINDER-QUOTIENT-ELIM, replace X by
(PLUS V (TIMES Z W)) to eliminate (REMAINDER X Z) and (QUOTIENT X Z).
We rely upon LESSP-REMAINDER2, the type restriction lemma noted when
REMAINDER was introduced, and the type restriction lemma noted when
QUOTIENT was introduced to restrict the new variables. We would thus
like to prove four new conjectures:
Case 4. (IMPLIES (AND (NOT (NUMBERP X))
(EQUAL (REMAINDER X Z) 0))
(EQUAL (REMAINDER (TIMES X Y) (TIMES Y Z))
0)),
which further simplifies, rewriting with EQUAL-TIMES-0, and opening
up LESSP, REMAINDER, and EQUAL, to:
T.
Case 3. (IMPLIES (AND (EQUAL Z 0)
(EQUAL (REMAINDER X Z) 0))
(EQUAL (REMAINDER (TIMES X Y) (TIMES Y Z))
0)),
which further simplifies, appealing to the lemmas
COMMUTATIVITY-OF-TIMES, REMAINDER-X-X, TIMES-IDENTITY, and
EQUAL-TIMES-0, and unfolding the definitions of EQUAL and REMAINDER,
to:
T.
Case 2. (IMPLIES (AND (NOT (NUMBERP Z))
(EQUAL (REMAINDER X Z) 0))
(EQUAL (REMAINDER (TIMES X Y) (TIMES Y Z))
0)),
which we further simplify, rewriting with REMAINDER-WRT-12,
TIMES-ZERO2, REMAINDER-TIMES, and EQUAL-TIMES-0, and opening up
EQUAL and REMAINDER, to:
T.
Case 1. (IMPLIES (AND (NUMBERP V)
(EQUAL (LESSP V Z) (NOT (ZEROP Z)))
(NUMBERP W)
(NUMBERP Z)
(NOT (EQUAL Z 0))
(EQUAL V 0))
(EQUAL (REMAINDER (TIMES (PLUS V (TIMES Z W)) Y)
(TIMES Y Z))
0)),
which further simplifies, applying COMMUTATIVITY-OF-TIMES,
ASSOCIATIVITY-OF-TIMES, and DIVIDES-TIMES, and expanding the
functions NUMBERP, EQUAL, LESSP, ZEROP, NOT, and PLUS, to:
T.
Q.E.D.
[ 8.277006 0.30799154 ]
PRODUCT-DIVIDES-LEMMA
(PROVE-LEMMA PRODUCT-DIVIDES
(REWRITE)
(IMPLIES (AND (EQUAL (REMAINDER X P) 0.)
(EQUAL (REMAINDER X Q) 0.)
(PRIME P)
(PRIME Q)
(NOT (EQUAL P Q)))
(EQUAL (REMAINDER X (TIMES P Q)) 0.)))
This conjecture can be simplified, using the abbreviations NOT, PRIME,
AND, and IMPLIES, to the new conjecture:
(IMPLIES (AND (EQUAL (REMAINDER X P) 0)
(EQUAL (REMAINDER X Q) 0)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(NOT (EQUAL Q 0))
(NUMBERP Q)
(NOT (EQUAL Q 1))
(PRIME1 Q (SUB1 Q))
(NOT (EQUAL P Q)))
(EQUAL (REMAINDER X (TIMES P Q)) 0)).
Appealing to the lemma REMAINDER-QUOTIENT-ELIM, we now replace X by
(PLUS Z (TIMES P V)) to eliminate (REMAINDER X P) and (QUOTIENT X P).
We use LESSP-REMAINDER2, the type restriction lemma noted when
REMAINDER was introduced, and the type restriction lemma noted when
QUOTIENT was introduced to constrain the new variables. We would
thus like to prove the following two new formulas:
Case 2. (IMPLIES (AND (NOT (NUMBERP X))
(EQUAL (REMAINDER X P) 0)
(EQUAL (REMAINDER X Q) 0)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(NOT (EQUAL Q 0))
(NUMBERP Q)
(NOT (EQUAL Q 1))
(PRIME1 Q (SUB1 Q))
(NOT (EQUAL P Q)))
(EQUAL (REMAINDER X (TIMES P Q)) 0)),
which simplifies, applying EQUAL-TIMES-0, and expanding the
definitions of LESSP, REMAINDER, and EQUAL, to:
T.
Case 1. (IMPLIES (AND (NUMBERP Z)
(EQUAL (LESSP Z P) (NOT (ZEROP P)))
(NUMBERP V)
(EQUAL Z 0)
(EQUAL (REMAINDER (PLUS Z (TIMES P V)) Q)
0)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(NOT (EQUAL Q 0))
(NUMBERP Q)
(NOT (EQUAL Q 1))
(PRIME1 Q (SUB1 Q))
(NOT (EQUAL P Q)))
(EQUAL (REMAINDER (PLUS Z (TIMES P V))
(TIMES P Q))
0)),
which simplifies, rewriting with LITTLE-STEP, PRIME-KEY-REWRITE,
and PRODUCT-DIVIDES-LEMMA, and opening up NUMBERP, EQUAL, LESSP,
ZEROP, NOT, PLUS, and PRIME, to:
T.
Q.E.D.
[ 41.5400105 0.31599121 ]
PRODUCT-DIVIDES
(PROVE-LEMMA THM-53-SPECIALIZED-TO-PRIMES NIL
(IMPLIES (AND (PRIME P)
(PRIME Q)
(NOT (EQUAL P Q))
(EQUAL (REMAINDER A P)
(REMAINDER B P))
(EQUAL (REMAINDER A Q)
(REMAINDER B Q)))
(EQUAL (REMAINDER A (TIMES P Q))
(REMAINDER B (TIMES P Q))))
NIL)
This conjecture can be simplified, using the abbreviations NOT, PRIME,
AND, and IMPLIES, to:
(IMPLIES (AND (NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(NOT (EQUAL Q 0))
(NUMBERP Q)
(NOT (EQUAL Q 1))
(PRIME1 Q (SUB1 Q))
(NOT (EQUAL P Q))
(EQUAL (REMAINDER A P)
(REMAINDER B P))
(EQUAL (REMAINDER A Q)
(REMAINDER B Q)))
(EQUAL (REMAINDER A (TIMES P Q))
(REMAINDER B (TIMES P Q)))),
which simplifies, rewriting with PRODUCT-DIVIDES, EQUAL-MODS-TRICK-2,
and EQUAL-MODS-TRICK-1, and opening up the functions EQUAL and PRIME,
to:
T.
Q.E.D.
[ 23.7170002 0.073006185 ]
THM-53-SPECIALIZED-TO-PRIMES
(PROVE-LEMMA COROLLARY-53
(REWRITE)
(IMPLIES (AND (PRIME P)
(PRIME Q)
(NOT (EQUAL P Q))
(EQUAL (REMAINDER A P)
(REMAINDER B P))
(EQUAL (REMAINDER A Q)
(REMAINDER B Q))
(NUMBERP B)
(LESSP B (TIMES P Q)))
(EQUAL (EQUAL (REMAINDER A (TIMES P Q)) B)
T))
((USE (THM-53-SPECIALIZED-TO-PRIMES))
(DISABLE THM-53-SPECIALIZED-TO-PRIMES)))
This formula can be simplified, using the abbreviations NOT, PRIME,
AND, and IMPLIES, to the new conjecture:
(IMPLIES
(AND (IMPLIES (AND (PRIME P)
(AND (PRIME Q)
(AND (NOT (EQUAL P Q))
(AND (EQUAL (REMAINDER A P)
(REMAINDER B P))
(EQUAL (REMAINDER A Q)
(REMAINDER B Q))))))
(EQUAL (REMAINDER A (TIMES P Q))
(REMAINDER B (TIMES P Q))))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(NOT (EQUAL Q 0))
(NUMBERP Q)
(NOT (EQUAL Q 1))
(PRIME1 Q (SUB1 Q))
(NOT (EQUAL P Q))
(EQUAL (REMAINDER A P)
(REMAINDER B P))
(EQUAL (REMAINDER A Q)
(REMAINDER B Q))
(NUMBERP B)
(LESSP B (TIMES P Q)))
(EQUAL (EQUAL (REMAINDER A (TIMES P Q)) B)
T)).
This simplifies, rewriting with EQUAL-TIMES-0, and opening up the
definitions of PRIME, NOT, AND, REMAINDER, and IMPLIES, to:
T.
Q.E.D.
[ 13.3660034 0.100996908 ]
COROLLARY-53
(PROVE-LEMMA THM-55-SPECIALIZED-TO-PRIMES
(REWRITE)
(IMPLIES (AND (PRIME P)
(NOT (EQUAL (REMAINDER M P) 0.)))
(EQUAL (EQUAL (REMAINDER (TIMES M X) P)
(REMAINDER (TIMES M Y) P))
(EQUAL (REMAINDER X P)
(REMAINDER Y P)))))
This conjecture can be simplified, using the abbreviations NOT, PRIME,
AND, and IMPLIES, to:
(IMPLIES (AND (NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(NOT (EQUAL (REMAINDER M P) 0)))
(EQUAL (EQUAL (REMAINDER (TIMES M X) P)
(REMAINDER (TIMES M Y) P))
(EQUAL (REMAINDER X P)
(REMAINDER Y P)))).
This simplifies, obviously, to the following two new conjectures:
Case 2. (IMPLIES (AND (NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(NOT (EQUAL (REMAINDER M P) 0))
(NOT (EQUAL (REMAINDER X P)
(REMAINDER Y P))))
(NOT (EQUAL (REMAINDER (TIMES M X) P)
(REMAINDER (TIMES M Y) P)))).
This simplifies again, applying PRIME-KEY-TRICK, and opening up
PRIME, to:
T.
Case 1. (IMPLIES (AND (NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(NOT (EQUAL (REMAINDER M P) 0))
(EQUAL (REMAINDER X P)
(REMAINDER Y P)))
(EQUAL (EQUAL (REMAINDER (TIMES M X) P)
(REMAINDER (TIMES M Y) P))
T)),
which we again simplify, rewriting with EQUAL-MODS-TRICK-2,
REMAINDER-EXP-LEMMA, and EQUAL-MODS-TRICK-1, and unfolding the
function EQUAL, to:
T.
Q.E.D.
[ 45.638005 0.14099528 ]
THM-55-SPECIALIZED-TO-PRIMES
(PROVE-LEMMA COROLLARY-55
(REWRITE)
(IMPLIES (PRIME P)
(EQUAL (EQUAL (REMAINDER (TIMES M X) P)
(REMAINDER M P))
(OR (EQUAL (REMAINDER M P) 0.)
(EQUAL (REMAINDER X P) 1.))))
((USE (THM-55-SPECIALIZED-TO-PRIMES (Y 1.)))
(DISABLE THM-55-SPECIALIZED-TO-PRIMES)))
This formula can be simplified, using the abbreviations PRIME and
IMPLIES, to:
(IMPLIES (AND (IMPLIES (AND (PRIME P)
(NOT (EQUAL (REMAINDER M P) 0)))
(EQUAL (EQUAL (REMAINDER (TIMES M X) P)
(REMAINDER (TIMES M 1) P))
(EQUAL (REMAINDER X P)
(REMAINDER 1 P))))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P)))
(EQUAL (EQUAL (REMAINDER (TIMES M X) P)
(REMAINDER M P))
(OR (EQUAL (REMAINDER M P) 0)
(EQUAL (REMAINDER X P) 1)))).
This simplifies, rewriting with TIMES-1, COMMUTATIVITY-OF-TIMES,
REMAINDER-OF-1, PRIME-KEY-REWRITE, EQUAL-TIMES-0, EQUAL-MODS-TRICK-2,
and EQUAL-MODS-TRICK-1, and opening up the definitions of PRIME, NOT,
AND, IMPLIES, EQUAL, OR, LESSP, and REMAINDER, to:
(IMPLIES (AND (NOT (EQUAL (REMAINDER X P) 1))
(NUMBERP M)
(NOT (EQUAL (REMAINDER (TIMES M X) P)
(REMAINDER M P)))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P)))
(NOT (EQUAL (REMAINDER M P) 0))).
However this again simplifies, applying the lemma PRIME-KEY-REWRITE,
and unfolding PRIME and EQUAL, to:
T.
Q.E.D.
[ 30.222001 0.129996745 ]
COROLLARY-55
(DEFN ALL-DISTINCT
(L)
(IF (NLISTP L)
T
(AND (NOT (MEMBER (CAR L) (CDR L)))
(ALL-DISTINCT (CDR L)))))
Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the
definition of NLISTP can be used to prove that the measure (COUNT L)
decreases according to the well-founded relation LESSP in each
recursive call. Hence, ALL-DISTINCT is accepted under the principle
of definition. Observe that:
(OR (FALSEP (ALL-DISTINCT L))
(TRUEP (ALL-DISTINCT L)))
is a theorem.
[ 1.76299642 0.069002279 ]
ALL-DISTINCT
(DEFN ALL-LESSEQP
(L N)
(IF (NLISTP L)
T
(AND ( LEQ (CAR L) N)
(ALL-LESSEQP (CDR L) N))))
Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the
definition of NLISTP can be used to prove that the measure (COUNT L)
decreases according to the well-founded relation LESSP in each
recursive call. Hence, ALL-LESSEQP is accepted under the principle
of definition. Observe that:
(OR (FALSEP (ALL-LESSEQP L N))
(TRUEP (ALL-LESSEQP L N)))
is a theorem.
[ 0.375 0.0540039064 ]
ALL-LESSEQP
(DEFN ALL-NON-ZEROP
(L)
(IF (NLISTP L)
T
(AND (NOT (ZEROP (CAR L)))
(ALL-NON-ZEROP (CDR L)))))
Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the
definition of NLISTP establish that the measure (COUNT L) decreases
according to the well-founded relation LESSP in each recursive call.
Hence, ALL-NON-ZEROP is accepted under the definitional principle.
From the definition we can conclude that:
(OR (FALSEP (ALL-NON-ZEROP L))
(TRUEP (ALL-NON-ZEROP L)))
is a theorem.
[ 0.46999512 0.0540039064 ]
ALL-NON-ZEROP
(DEFN POSITIVES
(N)
(IF (ZEROP N)
NIL
(CONS N (POSITIVES (SUB1 N)))))
Linear arithmetic, the lemma COUNT-NUMBERP, and the definition
of ZEROP establish that the measure (COUNT N) decreases according to
the well-founded relation LESSP in each recursive call. Hence,
POSITIVES is accepted under the principle of definition. Observe
that (OR (LITATOM (POSITIVES N)) (LISTP (POSITIVES N))) is a theorem.
[ 0.486995444 0.0460042316 ]
POSITIVES
(PROVE-LEMMA LISTP-POSITIVES
(REWRITE)
(EQUAL (LISTP (POSITIVES N))
(NOT (ZEROP N))))
This simplifies, opening up the functions ZEROP and NOT, to the
following three new goals:
Case 3. (IMPLIES (NOT (NUMBERP N))
(EQUAL (LISTP (POSITIVES N)) F)),
which again simplifies, opening up the definitions of POSITIVES,
LISTP, and EQUAL, to:
T.
Case 2. (IMPLIES (EQUAL N 0)
(EQUAL (LISTP (POSITIVES N)) F)),
which again simplifies, unfolding the functions POSITIVES, LISTP,
and EQUAL, to:
T.
Case 1. (IMPLIES (AND (NOT (EQUAL N 0)) (NUMBERP N))
(EQUAL (LISTP (POSITIVES N)) T)),
which we again simplify, obviously, to:
(IMPLIES (AND (NOT (EQUAL N 0)) (NUMBERP N))
(LISTP (POSITIVES N))),
which we will name *1.
We will appeal to induction. There is only one plausible
induction. We will induct according to the following scheme:
(AND (IMPLIES (ZEROP N) (P N))
(IMPLIES (AND (NOT (ZEROP N)) (P (SUB1 N)))
(P N))).
Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of
ZEROP establish that the measure (COUNT N) decreases according to the
well-founded relation LESSP in each induction step of the scheme.
The above induction scheme generates three new formulas:
Case 3. (IMPLIES (AND (ZEROP N)
(NOT (EQUAL N 0))
(NUMBERP N))
(LISTP (POSITIVES N))),
which we simplify, unfolding ZEROP, to:
T.
Case 2. (IMPLIES (AND (NOT (ZEROP N))
(EQUAL (SUB1 N) 0)
(NOT (EQUAL N 0))
(NUMBERP N))
(LISTP (POSITIVES N))).
This simplifies, opening up ZEROP and POSITIVES, to:
T.
Case 1. (IMPLIES (AND (NOT (ZEROP N))
(LISTP (POSITIVES (SUB1 N)))
(NOT (EQUAL N 0))
(NUMBERP N))
(LISTP (POSITIVES N))).
This simplifies, expanding ZEROP and POSITIVES, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.75698242 0.246020507 ]
LISTP-POSITIVES
(PROVE-LEMMA CAR-POSITIVES
(REWRITE)
(EQUAL (CAR (POSITIVES N))
(IF (ZEROP N) 0. N)))
This formula simplifies, expanding the function ZEROP, to three new
formulas:
Case 3. (IMPLIES (NOT (NUMBERP N))
(EQUAL (CAR (POSITIVES N)) 0)).
This simplifies again, expanding POSITIVES, CAR, and EQUAL, to:
T.
Case 2. (IMPLIES (EQUAL N 0)
(EQUAL (CAR (POSITIVES N)) 0)).
But this simplifies again, unfolding POSITIVES, CAR, and EQUAL, to:
T.
Case 1. (IMPLIES (AND (NOT (EQUAL N 0)) (NUMBERP N))
(EQUAL (CAR (POSITIVES N)) N)),
which we will name *1.
We will appeal to induction. There is only one plausible
induction. We will induct according to the following scheme:
(AND (IMPLIES (ZEROP N) (P N))
(IMPLIES (AND (NOT (ZEROP N)) (P (SUB1 N)))
(P N))).
Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of
ZEROP establish that the measure (COUNT N) decreases according to the
well-founded relation LESSP in each induction step of the scheme.
The above induction scheme generates three new formulas:
Case 3. (IMPLIES (AND (ZEROP N)
(NOT (EQUAL N 0))
(NUMBERP N))
(EQUAL (CAR (POSITIVES N)) N)),
which we simplify, unfolding ZEROP, to:
T.
Case 2. (IMPLIES (AND (NOT (ZEROP N))
(EQUAL (SUB1 N) 0)
(NOT (EQUAL N 0))
(NUMBERP N))
(EQUAL (CAR (POSITIVES N)) N)).
This simplifies, rewriting with the lemma CAR-CONS, and expanding
ZEROP and POSITIVES, to:
T.
Case 1. (IMPLIES (AND (NOT (ZEROP N))
(EQUAL (CAR (POSITIVES (SUB1 N)))
(SUB1 N))
(NOT (EQUAL N 0))
(NUMBERP N))
(EQUAL (CAR (POSITIVES N)) N)),
which we simplify, rewriting with the lemma CAR-CONS, and expanding
the definitions of ZEROP and POSITIVES, to:
T.
That finishes the proof of *1. Q.E.D.
[ 2.12298176 0.25201823 ]
CAR-POSITIVES
(PROVE-LEMMA MEMBER-POSITIVES
(REWRITE)
(EQUAL (MEMBER X (POSITIVES N))
(IF (ZEROP X) F (LESSP X (ADD1 N)))))
This conjecture simplifies, applying SUB1-ADD1, and expanding ZEROP
and LESSP, to the following four new goals:
Case 4. (IMPLIES (NOT (NUMBERP X))
(EQUAL (MEMBER X (POSITIVES N)) F)),
which again simplifies, obviously, to:
(IMPLIES (NOT (NUMBERP X))
(NOT (MEMBER X (POSITIVES N)))).
Name the above subgoal *1.
Case 3. (IMPLIES (EQUAL X 0)
(EQUAL (MEMBER X (POSITIVES N)) F)),
which we again simplify, trivially, to:
(NOT (MEMBER 0 (POSITIVES N))),
which we would normally push and work on later by induction. But
if we must use induction to prove the input conjecture, we prefer
to induct on the original formulation of the problem. Thus we will
disregard all that we have previously done, give the name *1 to the
original input, and work on it.
So now let us consider:
(EQUAL (MEMBER X (POSITIVES N))
(IF (ZEROP X) F (LESSP X (ADD1 N)))).
We gave this the name *1 above. We will appeal to induction. There
are two plausible inductions, both of which are unflawed. However,
one of these is more likely than the other. We will induct according
to the following scheme:
(AND (IMPLIES (ZEROP N) (P X N))
(IMPLIES (AND (NOT (ZEROP N)) (P X (SUB1 N)))
(P X N))).
Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of
ZEROP inform us that the measure (COUNT N) decreases according to the
well-founded relation LESSP in each induction step of the scheme.
The above induction scheme leads to the following two new formulas:
Case 2. (IMPLIES (ZEROP N)
(EQUAL (MEMBER X (POSITIVES N))
(IF (ZEROP X)
F
(LESSP X (ADD1 N))))),
which we simplify, rewriting with the lemma SUB1-TYPE-RESTRICTION,
and expanding the definitions of ZEROP, POSITIVES, LISTP, MEMBER,
and ADD1, to two new conjectures:
Case 2.2.
(IMPLIES (AND (EQUAL N 0)
(NOT (EQUAL X 0))
(NUMBERP X))
( LEQ 1 X)),
which we again simplify, using linear arithmetic, to:
T.
Case 2.1.
(IMPLIES (AND (NOT (NUMBERP N))
(NOT (EQUAL X 0))
(NUMBERP X))
( LEQ 1 X)),
which again simplifies, using linear arithmetic, to:
T.
Case 1. (IMPLIES (AND (NOT (ZEROP N))
(EQUAL (MEMBER X (POSITIVES (SUB1 N)))
(IF (ZEROP X)
F
(LESSP X (ADD1 (SUB1 N))))))
(EQUAL (MEMBER X (POSITIVES N))
(IF (ZEROP X)
F
(LESSP X (ADD1 N))))),
which simplifies, rewriting with ADD1-SUB1, CDR-CONS, CAR-CONS,
SUB1-ADD1, and EQUAL-LESSP, and expanding the definitions of ZEROP,
POSITIVES, MEMBER, EQUAL, and LESSP, to the following four new
formulas:
Case 1.4.
(IMPLIES (AND (NOT (EQUAL N 0))
(NUMBERP N)
(EQUAL X 0)
(EQUAL (MEMBER X (POSITIVES (SUB1 N)))
F))
(NOT (MEMBER 0 (POSITIVES (SUB1 N))))).
This simplifies again, obviously, to:
T.
Case 1.3.
(IMPLIES (AND (NOT (EQUAL N 0))
(NUMBERP N)
(NOT (EQUAL X 0))
(NUMBERP X)
(EQUAL (MEMBER X (POSITIVES (SUB1 N)))
(LESSP X N))
( LEQ N (SUB1 X)))
( LEQ N X)),
which we again simplify, using linear arithmetic, to:
T.
Case 1.2.
(IMPLIES (AND (NOT (EQUAL N 0))
(NUMBERP N)
(NOT (EQUAL X 0))
(NUMBERP X)
(EQUAL (MEMBER X (POSITIVES (SUB1 N)))
(LESSP X N))
( LEQ N (SUB1 X)))
(NOT (EQUAL X N))).
However this simplifies again, using linear arithmetic, to:
T.
Case 1.1.
(IMPLIES (AND (NOT (EQUAL N 0))
(NUMBERP N)
(NOT (EQUAL X 0))
(NUMBERP X)
(EQUAL (MEMBER X (POSITIVES (SUB1 N)))
(LESSP X N))
(LESSP (SUB1 X) N)
(NOT (EQUAL X N)))
(LESSP X N)),
which again simplifies, using linear arithmetic, to:
T.
That finishes the proof of *1. Q.E.D.
[ 3.02500814 0.533992514 ]
MEMBER-POSITIVES
(PROVE-LEMMA ALL-NON-ZEROP-DELETE
(REWRITE)
(IMPLIES (ALL-NON-ZEROP L)
(ALL-NON-ZEROP (DELETE X L))))
Name the conjecture *1.
We will try to prove it by induction. There are two plausible
inductions. However, they merge into one likely candidate induction.
We will induct according to the following scheme:
(AND (IMPLIES (NLISTP L) (P X L))
(IMPLIES (AND (NOT (NLISTP L)) (P X (CDR L)))
(P X L))).
Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the
definition of NLISTP inform us that the measure (COUNT L) decreases
according to the well-founded relation LESSP in each induction step
of the scheme. The above induction scheme generates the following
three new formulas:
Case 3. (IMPLIES (AND (NLISTP L) (ALL-NON-ZEROP L))
(ALL-NON-ZEROP (DELETE X L))),
which simplifies, applying DELETE-NON-MEMBER, and expanding the
definitions of NLISTP, ALL-NON-ZEROP, and MEMBER, to:
T.
Case 2. (IMPLIES (AND (NOT (NLISTP L))
(NOT (ALL-NON-ZEROP (CDR L)))
(ALL-NON-ZEROP L))
(ALL-NON-ZEROP (DELETE X L))),
which simplifies, unfolding the functions NLISTP and ALL-NON-ZEROP,
to:
T.
Case 1. (IMPLIES (AND (NOT (NLISTP L))
(ALL-NON-ZEROP (DELETE X (CDR L)))
(ALL-NON-ZEROP L))
(ALL-NON-ZEROP (DELETE X L))).
This simplifies, opening up the functions NLISTP, ALL-NON-ZEROP,
and DELETE, to the new conjecture:
(IMPLIES (AND (LISTP L)
(ALL-NON-ZEROP (DELETE X (CDR L)))
(NOT (EQUAL (CAR L) 0))
(NUMBERP (CAR L))
(ALL-NON-ZEROP (CDR L))
(NOT (EQUAL X (CAR L))))
(ALL-NON-ZEROP (CONS (CAR L) (DELETE X (CDR L))))),
which we again simplify, rewriting with CDR-CONS and CAR-CONS, and
opening up ALL-NON-ZEROP, to:
T.
That finishes the proof of *1. Q.E.D.
[ 1.75399576 0.252010092 ]
ALL-NON-ZEROP-DELETE
(PROVE-LEMMA ALL-DISTINCT-DELETE
(REWRITE)
(IMPLIES (ALL-DISTINCT L)
(ALL-DISTINCT (DELETE X L))))
Name the conjecture *1.
We will try to prove it by induction. There are two plausible
inductions. However, they merge into one likely candidate induction.
We will induct according to the following scheme:
(AND (IMPLIES (NLISTP L) (P X L))
(IMPLIES (AND (NOT (NLISTP L)) (P X (CDR L)))
(P X L))).
Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the
definition of NLISTP inform us that the measure (COUNT L) decreases
according to the well-founded relation LESSP in each induction step
of the scheme. The above induction scheme generates the following
three new formulas:
Case 3. (IMPLIES (AND (NLISTP L) (ALL-DISTINCT L))
(ALL-DISTINCT (DELETE X L))),
which simplifies, applying DELETE-NON-MEMBER, and expanding the
definitions of NLISTP, ALL-DISTINCT, and MEMBER, to:
T.
Case 2. (IMPLIES (AND (NOT (NLISTP L))
(NOT (ALL-DISTINCT (CDR L)))
(ALL-DISTINCT L))
(ALL-DISTINCT (DELETE X L))),
which simplifies, unfolding the functions NLISTP and ALL-DISTINCT,
to:
T.
Case 1. (IMPLIES (AND (NOT (NLISTP L))
(ALL-DISTINCT (DELETE X (CDR L)))
(ALL-DISTINCT L))
(ALL-DISTINCT (DELETE X L))).
This simplifies, opening up the functions NLISTP, ALL-DISTINCT, and
DELETE, to the new conjecture:
(IMPLIES (AND (LISTP L)
(ALL-DISTINCT (DELETE X (CDR L)))
(NOT (MEMBER (CAR L) (CDR L)))
(ALL-DISTINCT (CDR L))
(NOT (EQUAL X (CAR L))))
(ALL-DISTINCT (CONS (CAR L) (DELETE X (CDR L))))),
which we again simplify, rewriting with CDR-CONS and CAR-CONS, and
opening up ALL-DISTINCT, to:
(IMPLIES (AND (LISTP L)
(ALL-DISTINCT (DELETE X (CDR L)))
(NOT (MEMBER (CAR L) (CDR L)))
(ALL-DISTINCT (CDR L))
(NOT (EQUAL X (CAR L))))
(NOT (MEMBER (CAR L) (DELETE X (CDR L))))).
This simplifies again, rewriting with the lemma MEMBER-DELETE, to:
T.
That finishes the proof of *1. Q.E.D.
[ 1.14299317 0.27701009 ]
ALL-DISTINCT-DELETE
(PROVE-LEMMA PIGEON-HOLE-PRINCIPLE-LEMMA-1
(REWRITE)
(IMPLIES (AND (ALL-DISTINCT L)
(ALL-LESSEQP L (ADD1 N)))
(ALL-LESSEQP (DELETE (ADD1 N) L) N)))
Name the conjecture *1.
We will try to prove it by induction. There are three plausible
inductions. However, they merge into one likely candidate induction.
We will induct according to the following scheme:
(AND (IMPLIES (NLISTP L) (P N L))
(IMPLIES (AND (NOT (NLISTP L)) (P N (CDR L)))
(P N L))).
Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the
definition of NLISTP inform us that the measure (COUNT L) decreases
according to the well-founded relation LESSP in each induction step
of the scheme. The above induction scheme generates the following
four new formulas:
Case 4. (IMPLIES (AND (NLISTP L)
(ALL-DISTINCT L)
(ALL-LESSEQP L (ADD1 N)))
(ALL-LESSEQP (DELETE (ADD1 N) L) N)),
which simplifies, applying DELETE-NON-MEMBER, and expanding the
definitions of NLISTP, ALL-DISTINCT, ALL-LESSEQP, and MEMBER, to:
T.
Case 3. (IMPLIES (AND (NOT (NLISTP L))
(NOT (ALL-DISTINCT (CDR L)))
(ALL-DISTINCT L)
(ALL-LESSEQP L (ADD1 N)))
(ALL-LESSEQP (DELETE (ADD1 N) L) N)),
which simplifies, unfolding the functions NLISTP and ALL-DISTINCT,
to:
T.
Case 2. (IMPLIES (AND (NOT (NLISTP L))
(NOT (ALL-LESSEQP (CDR L) (ADD1 N)))
(ALL-DISTINCT L)
(ALL-LESSEQP L (ADD1 N)))
(ALL-LESSEQP (DELETE (ADD1 N) L) N)).
This simplifies, appealing to the lemma SUB1-ADD1, and opening up
NLISTP, ALL-DISTINCT, ALL-LESSEQP, and LESSP, to:
T.
Case 1. (IMPLIES (AND (NOT (NLISTP L))
(ALL-LESSEQP (DELETE (ADD1 N) (CDR L))
N)
(ALL-DISTINCT L)
(ALL-LESSEQP L (ADD1 N)))
(ALL-LESSEQP (DELETE (ADD1 N) L) N)).
This simplifies, applying SUB1-ADD1, CDR-CONS, CAR-CONS, and
SUB1-TYPE-RESTRICTION, and unfolding the functions NLISTP,
ALL-DISTINCT, ALL-LESSEQP, LESSP, DELETE, and EQUAL, to three new
conjectures:
Case 1.3.
(IMPLIES (AND (LISTP L)
(ALL-LESSEQP (DELETE (ADD1 N) (CDR L))
N)
(NOT (MEMBER (CAR L) (CDR L)))
(ALL-DISTINCT (CDR L))
(NUMBERP N)
( LEQ (SUB1 (CAR L)) N)
(ALL-LESSEQP (CDR L) (ADD1 N))
(NOT (EQUAL (ADD1 N) (CAR L))))
(ALL-LESSEQP (CONS (CAR L)
(DELETE (ADD1 N) (CDR L)))
N)).
This simplifies again, rewriting with the lemmas CDR-CONS and
CAR-CONS, and unfolding ALL-LESSEQP, to:
(IMPLIES (AND (LISTP L)
(ALL-LESSEQP (DELETE (ADD1 N) (CDR L))
N)
(NOT (MEMBER (CAR L) (CDR L)))
(ALL-DISTINCT (CDR L))
(NUMBERP N)
( LEQ (SUB1 (CAR L)) N)
(ALL-LESSEQP (CDR L) (ADD1 N))
(NOT (EQUAL (ADD1 N) (CAR L))))
( LEQ (CAR L) N)).
However this simplifies again, using linear arithmetic, to:
(IMPLIES (AND (NOT (NUMBERP (CAR L)))
(LISTP L)
(ALL-LESSEQP (DELETE (ADD1 N) (CDR L))
N)
(NOT (MEMBER (CAR L) (CDR L)))
(ALL-DISTINCT (CDR L))
(NUMBERP N)
( LEQ (SUB1 (CAR L)) N)
(ALL-LESSEQP (CDR L) (ADD1 N))
(NOT (EQUAL (ADD1 N) (CAR L))))
( LEQ (CAR L) N)).
However this again simplifies, rewriting with the lemma
SUB1-NNUMBERP, and unfolding the definitions of EQUAL and LESSP,
to:
T.
Case 1.2.
(IMPLIES (AND (LISTP L)
(ALL-LESSEQP (DELETE (ADD1 N) (CDR L))
N)
(NOT (MEMBER (CAR L) (CDR L)))
(ALL-DISTINCT (CDR L))
(NUMBERP N)
( LEQ (SUB1 (CAR L)) N)
(ALL-LESSEQP (CDR L) (ADD1 N))
(EQUAL (ADD1 N) (CAR L)))
(ALL-LESSEQP (CDR L) N)),
which again simplifies, rewriting with SUB1-ADD1, to:
(IMPLIES (AND (LISTP L)
(ALL-LESSEQP (DELETE (ADD1 N) (CDR L))
N)
(NOT (MEMBER (ADD1 N) (CDR L)))
(ALL-DISTINCT (CDR L))
(NUMBERP N)
( LEQ N N)
(ALL-LESSEQP (CDR L) (ADD1 N))
(EQUAL (ADD1 N) (CAR L)))
(ALL-LESSEQP (CDR L) N)),
which further simplifies, applying DELETE-NON-MEMBER, to:
T.
Case 1.1.
(IMPLIES (AND (LISTP L)
(ALL-LESSEQP (DELETE (ADD1 N) (CDR L))
N)
(NOT (MEMBER (CAR L) (CDR L)))
(ALL-DISTINCT (CDR L))
(NOT (NUMBERP N))
( LEQ (SUB1 (CAR L)) 0)
(ALL-LESSEQP (CDR L) (ADD1 N)))
(ALL-LESSEQP (DELETE 1 L) N)),
which again simplifies, unfolding the definitions of EQUAL and
LESSP, to:
(IMPLIES (AND (LISTP L)
(ALL-LESSEQP (DELETE (ADD1 N) (CDR L))
N)
(NOT (MEMBER (CAR L) (CDR L)))
(ALL-DISTINCT (CDR L))
(NOT (NUMBERP N))
(EQUAL (SUB1 (CAR L)) 0)
(ALL-LESSEQP (CDR L) (ADD1 N)))
(ALL-LESSEQP (DELETE 1 L) N)).
This further simplifies, rewriting with the lemma
SUB1-TYPE-RESTRICTION, to:
(IMPLIES (AND (LISTP L)
(ALL-LESSEQP (DELETE 1 (CDR L)) N)
(NOT (MEMBER (CAR L) (CDR L)))
(ALL-DISTINCT (CDR L))
(NOT (NUMBERP N))
(EQUAL (SUB1 (CAR L)) 0)
(ALL-LESSEQP (CDR L) 1))
(ALL-LESSEQP (DELETE 1 L) N)),
which again simplifies, expanding the function DELETE, to two new
conjectures:
Case 1.1.2.
(IMPLIES (AND (LISTP L)
(ALL-LESSEQP (DELETE 1 (CDR L)) N)
(NOT (MEMBER (CAR L) (CDR L)))
(ALL-DISTINCT (CDR L))
(NOT (NUMBERP N))
(EQUAL (SUB1 (CAR L)) 0)
(ALL-LESSEQP (CDR L) 1)
(NOT (EQUAL 1 (CAR L))))
(ALL-LESSEQP (CONS (CAR L) (DELETE 1 (CDR L)))
N)),
which we again simplify, using linear arithmetic, to two new
goals:
Case 1.1.2.2.
(IMPLIES (AND (LESSP (CAR L) 1)
(LISTP L)
(ALL-LESSEQP (DELETE 1 (CDR L)) N)
(NOT (MEMBER (CAR L) (CDR L)))
(ALL-DISTINCT (CDR L))
(NOT (NUMBERP N))
(EQUAL (SUB1 (CAR L)) 0)
(ALL-LESSEQP (CDR L) 1)
(NOT (EQUAL 1 (CAR L))))
(ALL-LESSEQP (CONS (CAR L) (DELETE 1 (CDR L)))
N)),
which we finally simplify, applying CDR-CONS, CAR-CONS, and
SUB1-NNUMBERP, and expanding LESSP, SUB1, NUMBERP, EQUAL, and
ALL-LESSEQP, to:
T.
Case 1.1.2.1.
(IMPLIES (AND (NOT (NUMBERP (CAR L)))
(LISTP L)
(ALL-LESSEQP (DELETE 1 (CDR L)) N)
(NOT (MEMBER (CAR L) (CDR L)))
(ALL-DISTINCT (CDR L))
(NOT (NUMBERP N))
(EQUAL (SUB1 (CAR L)) 0)
(ALL-LESSEQP (CDR L) 1)
(NOT (EQUAL 1 (CAR L))))
(ALL-LESSEQP (CONS (CAR L) (DELETE 1 (CDR L)))
N)),
which finally simplifies, rewriting with SUB1-NNUMBERP,
CDR-CONS, and CAR-CONS, and opening up the definitions of
EQUAL, LESSP, and ALL-LESSEQP, to:
T.
Case 1.1.1.
(IMPLIES (AND (LISTP L)
(ALL-LESSEQP (DELETE 1 (CDR L)) N)
(NOT (MEMBER (CAR L) (CDR L)))
(ALL-DISTINCT (CDR L))
(NOT (NUMBERP N))
(EQUAL (SUB1 (CAR L)) 0)
(ALL-LESSEQP (CDR L) 1)
(EQUAL 1 (CAR L)))
(ALL-LESSEQP (CDR L) N)),
which again simplifies, rewriting with the lemma
DELETE-NON-MEMBER, to:
T.
That finishes the proof of *1. Q.E.D.
[ 8.6469646 0.78203939 ]
PIGEON-HOLE-PRINCIPLE-LEMMA-1
(PROVE-LEMMA PIGEON-HOLE-PRINCIPLE-LEMMA-2
(REWRITE)
(IMPLIES (AND (NOT (MEMBER (ADD1 N) X))
(ALL-LESSEQP X (ADD1 N)))
(ALL-LESSEQP X N)))
Name the conjecture *1.
We will try to prove it by induction. There are three plausible
inductions. However, they merge into one likely candidate induction.
We will induct according to the following scheme:
(AND (IMPLIES (NLISTP X) (P X N))
(IMPLIES (AND (NOT (NLISTP X))
(EQUAL (ADD1 N) (CAR X)))
(P X N))
(IMPLIES (AND (NOT (NLISTP X))
(NOT (EQUAL (ADD1 N) (CAR X)))
(P (CDR X) N))
(P X N))).
Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the
definition of NLISTP inform us that the measure (COUNT X) decreases
according to the well-founded relation LESSP in each induction step
of the scheme. The above induction scheme generates the following
five new formulas:
Case 5. (IMPLIES (AND (NLISTP X)
(NOT (MEMBER (ADD1 N) X))
(ALL-LESSEQP X (ADD1 N)))
(ALL-LESSEQP X N)),
which simplifies, expanding the definitions of NLISTP, MEMBER, and
ALL-LESSEQP, to:
T.
Case 4. (IMPLIES (AND (NOT (NLISTP X))
(EQUAL (ADD1 N) (CAR X))
(NOT (MEMBER (ADD1 N) X))
(ALL-LESSEQP X (ADD1 N)))
(ALL-LESSEQP X N)),
which we simplify, unfolding NLISTP and MEMBER, to:
T.
Case 3. (IMPLIES (AND (NOT (NLISTP X))
(NOT (EQUAL (ADD1 N) (CAR X)))
(MEMBER (ADD1 N) (CDR X))
(NOT (MEMBER (ADD1 N) X))
(ALL-LESSEQP X (ADD1 N)))
(ALL-LESSEQP X N)),
which simplifies, unfolding the functions NLISTP and MEMBER, to:
T.
Case 2. (IMPLIES (AND (NOT (NLISTP X))
(NOT (EQUAL (ADD1 N) (CAR X)))
(NOT (ALL-LESSEQP (CDR X) (ADD1 N)))
(NOT (MEMBER (ADD1 N) X))
(ALL-LESSEQP X (ADD1 N)))
(ALL-LESSEQP X N)).
This simplifies, rewriting with SUB1-ADD1, and expanding NLISTP,
MEMBER, ALL-LESSEQP, and LESSP, to:
T.
Case 1. (IMPLIES (AND (NOT (NLISTP X))
(NOT (EQUAL (ADD1 N) (CAR X)))
(ALL-LESSEQP (CDR X) N)
(NOT (MEMBER (ADD1 N) X))
(ALL-LESSEQP X (ADD1 N)))
(ALL-LESSEQP X N)),
which we simplify, rewriting with the lemma SUB1-ADD1, and
expanding the definitions of NLISTP, MEMBER, ALL-LESSEQP, LESSP,
and EQUAL, to two new conjectures:
Case 1.2.
(IMPLIES (AND (LISTP X)
(NOT (EQUAL (ADD1 N) (CAR X)))
(ALL-LESSEQP (CDR X) N)
(NOT (MEMBER (ADD1 N) (CDR X)))
(NUMBERP N)
( LEQ (SUB1 (CAR X)) N)
(ALL-LESSEQP (CDR X) (ADD1 N)))
( LEQ (CAR X) N)),
which we again simplify, using linear arithmetic, to:
(IMPLIES (AND (NOT (NUMBERP (CAR X)))
(LISTP X)
(NOT (EQUAL (ADD1 N) (CAR X)))
(ALL-LESSEQP (CDR X) N)
(NOT (MEMBER (ADD1 N) (CDR X)))
(NUMBERP N)
( LEQ (SUB1 (CAR X)) N)
(ALL-LESSEQP (CDR X) (ADD1 N)))
( LEQ (CAR X) N)).
This again simplifies, rewriting with SUB1-NNUMBERP, and
expanding the definitions of EQUAL and LESSP, to:
T.
Case 1.1.
(IMPLIES (AND (LISTP X)
(NOT (EQUAL (ADD1 N) (CAR X)))
(ALL-LESSEQP (CDR X) N)
(NOT (MEMBER (ADD1 N) (CDR X)))
(NOT (NUMBERP N))
( LEQ (SUB1 (CAR X)) 0)
(ALL-LESSEQP (CDR X) (ADD1 N))
(NOT (EQUAL (CAR X) 0)))
(NOT (NUMBERP (CAR X)))).
However this again simplifies, using linear arithmetic, to the
new formula:
(IMPLIES (AND (EQUAL (CAR X) 1)
(LISTP X)
(NOT (EQUAL (ADD1 N) 1))
(ALL-LESSEQP (CDR X) N)
(NOT (MEMBER (ADD1 N) (CDR X)))
(NOT (NUMBERP N))
( LEQ (SUB1 1) 0)
(ALL-LESSEQP (CDR X) (ADD1 N))
(NOT (EQUAL 1 0)))
(NOT (NUMBERP 1))),
which we again simplify, applying SUB1-TYPE-RESTRICTION, and
unfolding EQUAL, to:
T.
That finishes the proof of *1. Q.E.D.
[ 1.52901204 1.21598308 ]
PIGEON-HOLE-PRINCIPLE-LEMMA-2
(PROVE-LEMMA PERM-MEMBER
(REWRITE)
(IMPLIES (AND (PERM A B) (MEMBER X A))
(MEMBER X B)))
WARNING: Note that PERM-MEMBER contains the free variable A which
will be chosen by instantiating the hypothesis (PERM A B).
Give the conjecture the name *1.
Let us appeal to the induction principle. The recursive terms
in the conjecture suggest four inductions. They merge into two
likely candidate inductions, both of which are unflawed. So we will
choose the one suggested by the largest number of nonprimitive
recursive functions. We will induct according to the following
scheme:
(AND (IMPLIES (NLISTP A) (P X B A))
(IMPLIES (AND (NOT (NLISTP A))
(MEMBER (CAR A) B)
(P X (DELETE (CAR A) B) (CDR A)))
(P X B A))
(IMPLIES (AND (NOT (NLISTP A))
(NOT (MEMBER (CAR A) B)))
(P X B A))).
Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the
definition of NLISTP inform us that the measure (COUNT A) decreases
according to the well-founded relation LESSP in each induction step
of the scheme. Note, however, the inductive instance chosen for B.
The above induction scheme generates five new conjectures:
Case 5. (IMPLIES (AND (NLISTP A)
(PERM A B)
(MEMBER X A))
(MEMBER X B)),
which simplifies, opening up the definitions of NLISTP, PERM, and
MEMBER, to:
T.
Case 4. (IMPLIES (AND (NOT (NLISTP A))
(MEMBER (CAR A) B)
(NOT (PERM (CDR A) (DELETE (CAR A) B)))
(PERM A B)
(MEMBER X A))
(MEMBER X B)).
This simplifies, expanding the functions NLISTP and PERM, to:
T.
Case 3. (IMPLIES (AND (NOT (NLISTP A))
(MEMBER (CAR A) B)
(NOT (MEMBER X (CDR A)))
(PERM A B)
(MEMBER X A))
(MEMBER X B)),
which we simplify, expanding the functions NLISTP, PERM, and MEMBER,
to:
(IMPLIES (AND (LISTP A)
(MEMBER (CAR A) B)
(NOT (MEMBER X (CDR A)))
(PERM (CDR A) (DELETE (CAR A) B))
(EQUAL X (CAR A)))
(MEMBER X B)),
which we again simplify, obviously, to:
T.
Case 2. (IMPLIES (AND (NOT (NLISTP A))
(MEMBER (CAR A) B)
(MEMBER X (DELETE (CAR A) B))
(PERM A B)
(MEMBER X A))
(MEMBER X B)),
which simplifies, appealing to the lemma MEMBER-DELETE, and
unfolding the definitions of NLISTP, PERM, and MEMBER, to:
T.
Case 1. (IMPLIES (AND (NOT (NLISTP A))
(NOT (MEMBER (CAR A) B))
(PERM A B)
(MEMBER X A))
(MEMBER X B)),
which we simplify, unfolding the functions NLISTP and PERM, to:
T.
That finishes the proof of *1. Q.E.D.
[ 1.90699056 0.319010418 ]
PERM-MEMBER
(DEFN PIGEON-HOLE-INDUCTION
(L)
(IF (LISTP L)
(IF (MEMBER (LENGTH L) L)
(PIGEON-HOLE-INDUCTION (DELETE (LENGTH L) L))
(PIGEON-HOLE-INDUCTION (CDR L)))
T))
Linear arithmetic and the lemmas LESSP-COUNT-DELETE and
CDR-LESSP establish that the measure (COUNT L) decreases according to
the well-founded relation LESSP in each recursive call. Hence,
PIGEON-HOLE-INDUCTION is accepted under the principle of definition.
Note that (TRUEP (PIGEON-HOLE-INDUCTION L)) is a theorem.
[ 0.74099935 0.067000326 ]
PIGEON-HOLE-INDUCTION
(PROVE-LEMMA PIGEON-HOLE-PRINCIPLE NIL
(IMPLIES (AND (ALL-NON-ZEROP L)
(ALL-DISTINCT L)
(ALL-LESSEQP L (LENGTH L)))
(PERM (POSITIVES (LENGTH L)) L))
((INDUCT (PIGEON-HOLE-INDUCTION L))))
This formula can be simplified, using the abbreviations IMPLIES, NOT,
OR, and AND, to the following three new goals:
Case 3. (IMPLIES
(AND
(LISTP L)
(MEMBER (LENGTH L) L)
(IMPLIES
(AND (ALL-NON-ZEROP (DELETE (LENGTH L) L))
(AND (ALL-DISTINCT (DELETE (LENGTH L) L))
(ALL-LESSEQP (DELETE (LENGTH L) L)
(LENGTH (DELETE (LENGTH L) L)))))
(PERM (POSITIVES (LENGTH (DELETE (LENGTH L) L)))
(DELETE (LENGTH L) L)))
(ALL-NON-ZEROP L)
(ALL-DISTINCT L)
(ALL-LESSEQP L (LENGTH L)))
(PERM (POSITIVES (LENGTH L)) L)).
This simplifies, rewriting with ALL-NON-ZEROP-DELETE,
ALL-DISTINCT-DELETE, and LENGTH-DELETE, and unfolding the functions
AND and IMPLIES, to two new conjectures:
Case 3.2.
(IMPLIES (AND (LISTP L)
(MEMBER (LENGTH L) L)
(NOT (ALL-LESSEQP (DELETE (LENGTH L) L)
(LENGTH (CDR L))))
(ALL-NON-ZEROP L)
(ALL-DISTINCT L)
(ALL-LESSEQP L (LENGTH L)))
(PERM (POSITIVES (LENGTH L)) L)).
However this again simplifies, applying the lemmas SUB1-ADD1,
CDR-CONS, and CAR-CONS, and unfolding LENGTH, POSITIVES, and PERM,
to:
(IMPLIES
(AND (LISTP L)
(MEMBER (ADD1 (LENGTH (CDR L))) L)
(NOT (ALL-LESSEQP (DELETE (ADD1 (LENGTH (CDR L))) L)
(LENGTH (CDR L))))
(ALL-NON-ZEROP L)
(ALL-DISTINCT L)
(ALL-LESSEQP L
(ADD1 (LENGTH (CDR L)))))
(PERM (POSITIVES (LENGTH (CDR L)))
(DELETE (ADD1 (LENGTH (CDR L))) L))).
This simplifies again, applying PIGEON-HOLE-PRINCIPLE-LEMMA-1, to:
T.
Case 3.1.
(IMPLIES (AND (LISTP L)
(MEMBER (LENGTH L) L)
(PERM (POSITIVES (LENGTH (CDR L)))
(DELETE (LENGTH L) L))
(ALL-NON-ZEROP L)
(ALL-DISTINCT L)
(ALL-LESSEQP L (LENGTH L)))
(PERM (POSITIVES (LENGTH L)) L)),
which again simplifies, rewriting with SUB1-ADD1, CDR-CONS, and
CAR-CONS, and opening up LENGTH, POSITIVES, and PERM, to:
T.
Case 2. (IMPLIES
(AND (LISTP L)
(NOT (MEMBER (LENGTH L) L))
(IMPLIES (AND (ALL-NON-ZEROP (CDR L))
(AND (ALL-DISTINCT (CDR L))
(ALL-LESSEQP (CDR L)
(LENGTH (CDR L)))))
(PERM (POSITIVES (LENGTH (CDR L)))
(CDR L)))
(ALL-NON-ZEROP L)
(ALL-DISTINCT L)
(ALL-LESSEQP L (LENGTH L)))
(PERM (POSITIVES (LENGTH L)) L)),
which simplifies, appealing to the lemmas SUB1-ADD1 and CAR-CONS,
and unfolding the definitions of LENGTH, AND, IMPLIES,
ALL-NON-ZEROP, ALL-DISTINCT, POSITIVES, and PERM, to two new
conjectures:
Case 2.2.
(IMPLIES (AND (LISTP L)
(NOT (MEMBER (ADD1 (LENGTH (CDR L))) L))
(NOT (ALL-LESSEQP (CDR L)
(LENGTH (CDR L))))
(NOT (EQUAL (CAR L) 0))
(NUMBERP (CAR L))
(ALL-NON-ZEROP (CDR L))
(NOT (MEMBER (CAR L) (CDR L)))
(ALL-DISTINCT (CDR L)))
(NOT (ALL-LESSEQP L
(ADD1 (LENGTH (CDR L)))))).
Applying the lemma CAR-CDR-ELIM, we now replace L by (CONS Z X)
to eliminate (CDR L) and (CAR L). This produces:
(IMPLIES (AND (NOT (MEMBER (ADD1 (LENGTH X)) (CONS Z X)))
(NOT (ALL-LESSEQP X (LENGTH X)))
(NOT (EQUAL Z 0))
(NUMBERP Z)
(ALL-NON-ZEROP X)
(NOT (MEMBER Z X))
(ALL-DISTINCT X))
(NOT (ALL-LESSEQP (CONS Z X)
(ADD1 (LENGTH X))))).
This simplifies further, rewriting with the lemmas CDR-CONS,
CAR-CONS, and SUB1-ADD1, and unfolding MEMBER, LESSP, and
ALL-LESSEQP, to:
(IMPLIES (AND (NOT (EQUAL (ADD1 (LENGTH X)) Z))
(NOT (MEMBER (ADD1 (LENGTH X)) X))
(NOT (ALL-LESSEQP X (LENGTH X)))
(NOT (EQUAL Z 0))
(NUMBERP Z)
(ALL-NON-ZEROP X)
(NOT (MEMBER Z X))
(ALL-DISTINCT X)
( LEQ (SUB1 Z) (LENGTH X)))
(NOT (ALL-LESSEQP X (ADD1 (LENGTH X))))).
However this simplifies again, applying
PIGEON-HOLE-PRINCIPLE-LEMMA-2, to:
T.
Case 2.1.
(IMPLIES (AND (LISTP L)
(NOT (MEMBER (ADD1 (LENGTH (CDR L))) L))
(PERM (POSITIVES (LENGTH (CDR L)))
(CDR L))
(NOT (EQUAL (CAR L) 0))
(NUMBERP (CAR L))
(ALL-NON-ZEROP (CDR L))
(NOT (MEMBER (CAR L) (CDR L)))
(ALL-DISTINCT (CDR L)))
(NOT (ALL-LESSEQP L
(ADD1 (LENGTH (CDR L)))))).
Appealing to the lemma CAR-CDR-ELIM, we now replace L by
(CONS Z X) to eliminate (CDR L) and (CAR L). The result is the
new formula:
(IMPLIES (AND (NOT (MEMBER (ADD1 (LENGTH X)) (CONS Z X)))
(PERM (POSITIVES (LENGTH X)) X)
(NOT (EQUAL Z 0))
(NUMBERP Z)
(ALL-NON-ZEROP X)
(NOT (MEMBER Z X))
(ALL-DISTINCT X))
(NOT (ALL-LESSEQP (CONS Z X)
(ADD1 (LENGTH X))))),
which we further simplify, applying CDR-CONS, CAR-CONS, and
SUB1-ADD1, and unfolding MEMBER, LESSP, and ALL-LESSEQP, to the
conjecture:
(IMPLIES (AND (NOT (EQUAL (ADD1 (LENGTH X)) Z))
(NOT (MEMBER (ADD1 (LENGTH X)) X))
(PERM (POSITIVES (LENGTH X)) X)
(NOT (EQUAL Z 0))
(NUMBERP Z)
(ALL-NON-ZEROP X)
(NOT (MEMBER Z X))
(ALL-DISTINCT X)
( LEQ (SUB1 Z) (LENGTH X)))
(NOT (ALL-LESSEQP X (ADD1 (LENGTH X))))),
which again simplifies, using linear arithmetic and rewriting
with MEMBER-POSITIVES and PERM-MEMBER, to:
T.
Case 1. (IMPLIES (AND (NOT (LISTP L))
(ALL-NON-ZEROP L)
(ALL-DISTINCT L)
(ALL-LESSEQP L (LENGTH L)))
(PERM (POSITIVES (LENGTH L)) L)).
This simplifies, applying the lemma PIGEON-HOLE-PRINCIPLE-LEMMA-2,
and opening up the functions ALL-NON-ZEROP, ALL-DISTINCT, LENGTH,
ALL-LESSEQP, MEMBER, ADD1, POSITIVES, LISTP, and PERM, to:
T.
Q.E.D.
[ 23.0870118 0.60999349 ]
PIGEON-HOLE-PRINCIPLE
(PROVE-LEMMA PERM-TIMES-LIST NIL
(IMPLIES (PERM L1 L2)
(EQUAL (TIMES-LIST L1)
(TIMES-LIST L2))))
Give the conjecture the name *1.
We will appeal to induction. There are four plausible
inductions. They merge into two likely candidate inductions, both of
which are unflawed. So we will choose the one suggested by the
largest number of nonprimitive recursive functions. We will induct
according to the following scheme:
(AND (IMPLIES (NLISTP L1) (P L1 L2))
(IMPLIES (AND (NOT (NLISTP L1))
(MEMBER (CAR L1) L2)
(P (CDR L1) (DELETE (CAR L1) L2)))
(P L1 L2))
(IMPLIES (AND (NOT (NLISTP L1))
(NOT (MEMBER (CAR L1) L2)))
(P L1 L2))).
Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the
definition of NLISTP can be used to establish that the measure
(COUNT L1) decreases according to the well-founded relation LESSP in
each induction step of the scheme. Note, however, the inductive
instance chosen for L2. The above induction scheme produces four new
conjectures:
Case 4. (IMPLIES (AND (NLISTP L1) (PERM L1 L2))
(EQUAL (TIMES-LIST L1)
(TIMES-LIST L2))).
This simplifies, opening up the functions NLISTP, PERM, TIMES-LIST,
and EQUAL, to:
T.
Case 3. (IMPLIES (AND (NOT (NLISTP L1))
(MEMBER (CAR L1) L2)
(NOT (PERM (CDR L1) (DELETE (CAR L1) L2)))
(PERM L1 L2))
(EQUAL (TIMES-LIST L1)
(TIMES-LIST L2))),
which simplifies, rewriting with PERM-MEMBER, and expanding the
functions NLISTP, MEMBER, and PERM, to:
T.
Case 2. (IMPLIES (AND (NOT (NLISTP L1))
(MEMBER (CAR L1) L2)
(EQUAL (TIMES-LIST (CDR L1))
(TIMES-LIST (DELETE (CAR L1) L2)))
(PERM L1 L2))
(EQUAL (TIMES-LIST L1)
(TIMES-LIST L2))),
which we simplify, applying PERM-MEMBER, and opening up NLISTP,
MEMBER, PERM, and TIMES-LIST, to:
(IMPLIES (AND (LISTP L1)
(EQUAL (TIMES-LIST (CDR L1))
(TIMES-LIST (DELETE (CAR L1) L2)))
(MEMBER (CAR L1) L2)
(PERM (CDR L1) (DELETE (CAR L1) L2)))
(EQUAL (TIMES (CAR L1) (TIMES-LIST (CDR L1)))
(TIMES-LIST L2))).
Applying the lemma CAR-CDR-ELIM, replace L1 by (CONS Z X) to
eliminate (CDR L1) and (CAR L1). This produces the goal:
(IMPLIES (AND (EQUAL (TIMES-LIST X)
(TIMES-LIST (DELETE Z L2)))
(MEMBER Z L2)
(PERM X (DELETE Z L2)))
(EQUAL (TIMES Z (TIMES-LIST X))
(TIMES-LIST L2))).
We now use the above equality hypothesis by substituting:
(TIMES-LIST (DELETE Z L2))
for (TIMES-LIST X) and throwing away the equality. The result is:
(IMPLIES (AND (MEMBER Z L2)
(PERM X (DELETE Z L2)))
(EQUAL (TIMES Z (TIMES-LIST (DELETE Z L2)))
(TIMES-LIST L2))),
which we further simplify, rewriting with the lemma
TIMES-TIMES-LIST-DELETE, to:
T.
Case 1. (IMPLIES (AND (NOT (NLISTP L1))
(NOT (MEMBER (CAR L1) L2))
(PERM L1 L2))
(EQUAL (TIMES-LIST L1)
(TIMES-LIST L2))),
which simplifies, applying PERM-MEMBER, and expanding the functions
NLISTP and MEMBER, to:
T.
That finishes the proof of *1. Q.E.D.
[ 4.9910075 0.40498047 ]
PERM-TIMES-LIST
(PROVE-LEMMA TIMES-LIST-POSITIVES
(REWRITE)
(EQUAL (TIMES-LIST (POSITIVES N))
(FACT N)))
Name the conjecture *1.
Perhaps we can prove it by induction. The recursive terms in
the conjecture suggest two inductions. However, they merge into one
likely candidate induction. We will induct according to the
following scheme:
(AND (IMPLIES (ZEROP N) (P N))
(IMPLIES (AND (NOT (ZEROP N)) (P (SUB1 N)))
(P N))).
Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of
ZEROP inform us that the measure (COUNT N) decreases according to the
well-founded relation LESSP in each induction step of the scheme.
The above induction scheme produces two new formulas:
Case 2. (IMPLIES (ZEROP N)
(EQUAL (TIMES-LIST (POSITIVES N))
(FACT N))).
This simplifies, opening up the definitions of ZEROP, POSITIVES,
TIMES-LIST, FACT, and EQUAL, to:
T.
Case 1. (IMPLIES (AND (NOT (ZEROP N))
(EQUAL (TIMES-LIST (POSITIVES (SUB1 N)))
(FACT (SUB1 N))))
(EQUAL (TIMES-LIST (POSITIVES N))
(FACT N))),
which we simplify, rewriting with the lemmas CDR-CONS and CAR-CONS,
and unfolding the functions ZEROP, POSITIVES, TIMES-LIST, and FACT,
to:
T.
That finishes the proof of *1. Q.E.D.
[ 1.12799479 0.161995443 ]
TIMES-LIST-POSITIVES
(PROVE-LEMMA TIMES-LIST-EQUAL-FACT
(REWRITE)
(IMPLIES (PERM (POSITIVES N) L)
(EQUAL (TIMES-LIST L) (FACT N)))
((USE (PERM-TIMES-LIST (L1 (POSITIVES N))
(L2 L)))
(DISABLE PERM-TIMES-LIST)))
WARNING: Note that TIMES-LIST-EQUAL-FACT contains the free variable
N which will be chosen by instantiating the hypothesis
(PERM (POSITIVES N) L).
This formula can be simplified, using the abbreviations IMPLIES and
TIMES-LIST-POSITIVES, to:
(IMPLIES (AND (IMPLIES (PERM (POSITIVES N) L)
(EQUAL (FACT N) (TIMES-LIST L)))
(PERM (POSITIVES N) L))
(EQUAL (TIMES-LIST L) (FACT N))).
This simplifies, expanding the definition of IMPLIES, to:
T.
Q.E.D.
[ 0.72600098 0.0420003254 ]
TIMES-LIST-EQUAL-FACT
(PROVE-LEMMA PRIME-FACT
(REWRITE)
(IMPLIES (AND (PRIME P) (LESSP N P))
(NOT (EQUAL (REMAINDER (FACT N) P) 0.)))
((INDUCT (FACT N))))
This formula can be simplified, using the abbreviations ZEROP, PRIME,
IMPLIES, NOT, OR, and AND, to the following two new goals:
Case 2. (IMPLIES (AND (ZEROP N)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(LESSP N P))
(NOT (EQUAL (REMAINDER (FACT N) P) 0))),
which we simplify, applying REMAINDER-OF-1, and unfolding the
functions ZEROP, EQUAL, LESSP, and FACT, to:
T.
Case 1. (IMPLIES
(AND (NOT (EQUAL N 0))
(NUMBERP N)
(IMPLIES (AND (PRIME P) (LESSP (SUB1 N) P))
(NOT (EQUAL (REMAINDER (FACT (SUB1 N)) P)
0)))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(LESSP N P))
(NOT (EQUAL (REMAINDER (FACT N) P) 0))),
which we simplify, rewriting with PRIME-KEY-REWRITE, and unfolding
the definitions of PRIME, AND, NOT, IMPLIES, LESSP, FACT, and
REMAINDER, to the new conjecture:
(IMPLIES (AND (NOT (EQUAL N 0))
(NUMBERP N)
( LEQ P (SUB1 N))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(LESSP (SUB1 N) (SUB1 P)))
(NOT (EQUAL (REMAINDER (FACT (SUB1 N)) P)
0))),
which we again simplify, using linear arithmetic, to:
T.
Q.E.D.
[ 11.620988 0.15201009 ]
PRIME-FACT
(DEFN S
(N M P)
(IF (ZEROP N)
NIL
(CONS (REMAINDER (TIMES M N) P)
(S (SUB1 N) M P))))
Linear arithmetic, the lemma COUNT-NUMBERP, and the definition
of ZEROP inform us that the measure (COUNT N) decreases according to
the well-founded relation LESSP in each recursive call. Hence, S is
accepted under the principle of definition. Observe that:
(OR (LITATOM (S N M P))
(LISTP (S N M P)))
is a theorem.
[ 0.225008138 0.047989909 ]
S
(PROVE-LEMMA REMAINDER-TIMES-LIST-S NIL
(EQUAL (REMAINDER (TIMES-LIST (S N M P)) P)
(REMAINDER (TIMES (FACT N) (EXP M N))
P)))
Give the conjecture the name *1.
We will try to prove it by induction. Three inductions are
suggested by terms in the conjecture. However, they merge into one
likely candidate induction. We will induct according to the
following scheme:
(AND (IMPLIES (ZEROP N) (P N M P))
(IMPLIES (AND (NOT (ZEROP N)) (P (SUB1 N) M P))
(P N M P))).
Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of
ZEROP inform us that the measure (COUNT N) decreases according to the
well-founded relation LESSP in each induction step of the scheme.
The above induction scheme leads to the following two new goals:
Case 2. (IMPLIES (ZEROP N)
(EQUAL (REMAINDER (TIMES-LIST (S N M P)) P)
(REMAINDER (TIMES (FACT N) (EXP M N))
P))),
which we simplify, applying REMAINDER-OF-1 and EXP-BY-0, and
unfolding the functions ZEROP, EQUAL, S, TIMES-LIST, FACT, TIMES,
and EXP, to:
T.
Case 1. (IMPLIES (AND (NOT (ZEROP N))
(EQUAL (REMAINDER (TIMES-LIST (S (SUB1 N) M P))
P)
(REMAINDER (TIMES (FACT (SUB1 N))
(EXP M (SUB1 N)))
P)))
(EQUAL (REMAINDER (TIMES-LIST (S N M P)) P)
(REMAINDER (TIMES (FACT N) (EXP M N))
P))),
which we simplify, rewriting with CDR-CONS, CAR-CONS,
ASSOCIATIVITY-OF-TIMES, TIMES-MOD-3, COMMUTATIVITY2-OF-TIMES,
EQUAL-MODS-TRICK-2, REMAINDER-EXP-LEMMA, and EQUAL-MODS-TRICK-1,
and unfolding the definitions of ZEROP, S, TIMES-LIST, FACT, EXP,
and EQUAL, to:
T.
That finishes the proof of *1. Q.E.D.
[ 16.9879963 0.202001953 ]
REMAINDER-TIMES-LIST-S
(PROVE-LEMMA ALL-DISTINCT-S-LEMMA
(REWRITE)
(IMPLIES (AND (PRIME P)
(NOT (EQUAL (REMAINDER M P) 0.))
(NUMBERP N1)
(LESSP N2 N1)
(LESSP N1 P))
(NOT (MEMBER (REMAINDER (TIMES M N1) P)
(S N2 M P))))
((INDUCT (S N2 M P))))
This formula can be simplified, using the abbreviations ZEROP, PRIME,
IMPLIES, NOT, OR, and AND, to the following two new formulas:
Case 2. (IMPLIES (AND (ZEROP N2)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(NOT (EQUAL (REMAINDER M P) 0))
(NUMBERP N1)
(LESSP N2 N1)
(LESSP N1 P))
(NOT (MEMBER (REMAINDER (TIMES M N1) P)
(S N2 M P)))).
This simplifies, expanding ZEROP, EQUAL, LESSP, S, LISTP, and
MEMBER, to:
T.
Case 1. (IMPLIES
(AND (NOT (EQUAL N2 0))
(NUMBERP N2)
(IMPLIES (AND (PRIME P)
(AND (NOT (EQUAL (REMAINDER M P) 0))
(AND (NUMBERP N1)
(AND (LESSP (SUB1 N2) N1)
(LESSP N1 P)))))
(NOT (MEMBER (REMAINDER (TIMES M N1) P)
(S (SUB1 N2) M P))))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(NOT (EQUAL (REMAINDER M P) 0))
(NUMBERP N1)
(LESSP N2 N1)
(LESSP N1 P))
(NOT (MEMBER (REMAINDER (TIMES M N1) P)
(S N2 M P)))).
This simplifies, using linear arithmetic, applying the lemmas
CDR-CONS, THM-55-SPECIALIZED-TO-PRIMES, DIFFERENCE-0,
REMAINDER-0-CROCK, and CAR-CONS, and expanding the definitions of
PRIME, NOT, AND, IMPLIES, S, LESSP, REMAINDER, and MEMBER, to five
new formulas:
Case 1.5.
(IMPLIES (AND (NOT (EQUAL N2 0))
(NUMBERP N2)
( LEQ N1 (SUB1 N2))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(NOT (EQUAL (REMAINDER M P) 0))
(NUMBERP N1)
(LESSP N2 N1)
(LESSP N1 P)
( LEQ (SUB1 P) (SUB1 N2)))
(NOT (EQUAL N1 0))),
which we again simplify, using linear arithmetic, to:
T.
Case 1.4.
(IMPLIES (AND (NOT (EQUAL N2 0))
(NUMBERP N2)
( LEQ N1 (SUB1 N2))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(NOT (EQUAL (REMAINDER M P) 0))
(NUMBERP N1)
(LESSP N2 N1)
(LESSP N1 P)
(LESSP (SUB1 N2) (SUB1 P)))
(NOT (EQUAL N1 N2))).
However this again simplifies, using linear arithmetic, to:
T.
Case 1.3.
(IMPLIES (AND (NOT (EQUAL N2 0))
(NUMBERP N2)
( LEQ N1 (SUB1 N2))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(NOT (EQUAL (REMAINDER M P) 0))
(NUMBERP N1)
(LESSP N2 N1)
(LESSP N1 P))
(NOT (MEMBER (REMAINDER (TIMES M N1) P)
(S (SUB1 N2) M P)))).
But this simplifies again, using linear arithmetic, to:
T.
Case 1.2.
(IMPLIES (AND (NOT (EQUAL N2 0))
(NUMBERP N2)
(NOT (MEMBER (REMAINDER (TIMES M N1) P)
(S (SUB1 N2) M P)))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(NOT (EQUAL (REMAINDER M P) 0))
(NUMBERP N1)
(LESSP N2 N1)
(LESSP N1 P)
( LEQ (SUB1 P) (SUB1 N2)))
(NOT (EQUAL N1 0))).
However this simplifies again, using linear arithmetic, to:
T.
Case 1.1.
(IMPLIES (AND (NOT (EQUAL N2 0))
(NUMBERP N2)
(NOT (MEMBER (REMAINDER (TIMES M N1) P)
(S (SUB1 N2) M P)))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(NOT (EQUAL (REMAINDER M P) 0))
(NUMBERP N1)
(LESSP N2 N1)
(LESSP N1 P)
(LESSP (SUB1 N2) (SUB1 P)))
(NOT (EQUAL N1 N2))),
which we again simplify, using linear arithmetic, to:
T.
Q.E.D.
[ 23.8640056 0.370996095 ]
ALL-DISTINCT-S-LEMMA
(PROVE-LEMMA ALL-DISTINCT-S
(REWRITE)
(IMPLIES (AND (PRIME P)
(NOT (EQUAL (REMAINDER M P) 0.))
(LESSP N P))
(ALL-DISTINCT (S N M P))))
This conjecture can be simplified, using the abbreviations NOT, PRIME,
AND, and IMPLIES, to:
(IMPLIES (AND (NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(NOT (EQUAL (REMAINDER M P) 0))
(LESSP N P))
(ALL-DISTINCT (S N M P))).
Appealing to the lemma REMAINDER-QUOTIENT-ELIM, replace M by
(PLUS X (TIMES P Z)) to eliminate (REMAINDER M P) and (QUOTIENT M P).
We rely upon LESSP-REMAINDER2, the type restriction lemma noted when
REMAINDER was introduced, and the type restriction lemma noted when
QUOTIENT was introduced to constrain the new variables. The result
is two new goals:
Case 2. (IMPLIES (AND (NOT (NUMBERP M))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(NOT (EQUAL (REMAINDER M P) 0))
(LESSP N P))
(ALL-DISTINCT (S N M P))),
which we simplify, unfolding LESSP, REMAINDER, and EQUAL, to:
T.
Case 1. (IMPLIES (AND (NUMBERP X)
(EQUAL (LESSP X P) (NOT (ZEROP P)))
(NUMBERP Z)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(NOT (EQUAL X 0))
(LESSP N P))
(ALL-DISTINCT (S N (PLUS X (TIMES P Z)) P))),
which simplifies, expanding the definitions of ZEROP and NOT, to:
(IMPLIES (AND (NUMBERP X)
(LESSP X P)
(NUMBERP Z)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(NOT (EQUAL X 0))
(LESSP N P))
(ALL-DISTINCT (S N (PLUS X (TIMES P Z)) P))).
Applying the lemma SUB1-ELIM, replace P by (ADD1 V) to eliminate
(SUB1 P). We employ the type restriction lemma noted when SUB1 was
introduced to constrain the new variable. We must thus prove:
(IMPLIES (AND (NUMBERP V)
(NUMBERP X)
(LESSP X (ADD1 V))
(NUMBERP Z)
(NOT (EQUAL (ADD1 V) 0))
(NOT (EQUAL (ADD1 V) 1))
(PRIME1 (ADD1 V) V)
(NOT (EQUAL X 0))
(LESSP N (ADD1 V)))
(ALL-DISTINCT (S N
(PLUS X (TIMES (ADD1 V) Z))
(ADD1 V)))).
But this further simplifies, rewriting with SUB1-ADD1, ADD1-EQUAL,
COMMUTATIVITY-OF-TIMES, and TIMES-ADD1, and expanding LESSP,
NUMBERP, EQUAL, S, and ALL-DISTINCT, to:
(IMPLIES (AND (NUMBERP V)
(NUMBERP X)
(LESSP (SUB1 X) V)
(NUMBERP Z)
(NOT (EQUAL V 0))
(PRIME1 (ADD1 V) V)
(NOT (EQUAL X 0))
(LESSP (SUB1 N) V))
(ALL-DISTINCT (S N
(PLUS X (PLUS Z (TIMES V Z)))
(ADD1 V)))).
Applying the lemma SUB1-ELIM, we now replace N by (ADD1 W) to
eliminate (SUB1 N). We employ the type restriction lemma noted
when SUB1 was introduced to constrain the new variable. The result
is three new conjectures:
Case 1.3.
(IMPLIES (AND (EQUAL N 0)
(NUMBERP V)
(NUMBERP X)
(LESSP (SUB1 X) V)
(NUMBERP Z)
(NOT (EQUAL V 0))
(PRIME1 (ADD1 V) V)
(NOT (EQUAL X 0))
(LESSP (SUB1 N) V))
(ALL-DISTINCT (S N
(PLUS X (PLUS Z (TIMES V Z)))
(ADD1 V)))),
which we finally simplify, unfolding SUB1, EQUAL, LESSP, S, and
ALL-DISTINCT, to:
T.
Case 1.2.
(IMPLIES (AND (NOT (NUMBERP N))
(NUMBERP V)
(NUMBERP X)
(LESSP (SUB1 X) V)
(NUMBERP Z)
(NOT (EQUAL V 0))
(PRIME1 (ADD1 V) V)
(NOT (EQUAL X 0))
(LESSP (SUB1 N) V))
(ALL-DISTINCT (S N
(PLUS X (PLUS Z (TIMES V Z)))
(ADD1 V)))),
which finally simplifies, rewriting with SUB1-NNUMBERP, and
expanding the definitions of EQUAL, LESSP, S, and ALL-DISTINCT,
to:
T.
Case 1.1.
(IMPLIES (AND (NUMBERP W)
(NOT (EQUAL (ADD1 W) 0))
(NUMBERP V)
(NUMBERP X)
(LESSP (SUB1 X) V)
(NUMBERP Z)
(NOT (EQUAL V 0))
(PRIME1 (ADD1 V) V)
(NOT (EQUAL X 0))
(LESSP W V))
(ALL-DISTINCT (S (ADD1 W)
(PLUS X (PLUS Z (TIMES V Z)))
(ADD1 V)))).
However this further simplifies, rewriting with the lemmas
SUB1-ADD1, ASSOCIATIVITY-OF-PLUS, COMMUTATIVITY2-OF-PLUS,
COMMUTATIVITY2-OF-TIMES, DISTRIBUTIVITY-OF-TIMES-OVER-PLUS,
TIMES-ADD1, COMMUTATIVITY-OF-TIMES, CDR-CONS, and CAR-CONS, and
unfolding the definitions of S and ALL-DISTINCT, to two new
conjectures:
Case 1.1.2.
(IMPLIES
(AND (NUMBERP W)
(NUMBERP V)
(NUMBERP X)
(LESSP (SUB1 X) V)
(NUMBERP Z)
(NOT (EQUAL V 0))
(PRIME1 (ADD1 V) V)
(NOT (EQUAL X 0))
(LESSP W V))
(NOT
(MEMBER
(REMAINDER
(PLUS X
(PLUS Z
(PLUS (TIMES V Z)
(PLUS (TIMES W X)
(PLUS (TIMES W Z)
(TIMES V (TIMES W Z)))))))
(ADD1 V))
(S W
(PLUS X (PLUS Z (TIMES V Z)))
(ADD1 V))))),
which we would normally push and work on later by induction.
But if we must use induction to prove the input conjecture, we
prefer to induct on the original formulation of the problem.
Thus we will disregard all that we have previously done, give
the name *1 to the original input, and work on it.
So now let us consider:
(IMPLIES (AND (PRIME P)
(NOT (EQUAL (REMAINDER M P) 0))
(LESSP N P))
(ALL-DISTINCT (S N M P))),
named *1. We will try to prove it by induction. Four inductions are
suggested by terms in the conjecture. They merge into three likely
candidate inductions. However, only one is unflawed. We will induct
according to the following scheme:
(AND (IMPLIES (ZEROP N) (P N M P))
(IMPLIES (AND (NOT (ZEROP N)) (P (SUB1 N) M P))
(P N M P))).
Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of
ZEROP inform us that the measure (COUNT N) decreases according to the
well-founded relation LESSP in each induction step of the scheme.
The above induction scheme leads to the following three new
conjectures:
Case 3. (IMPLIES (AND (ZEROP N)
(PRIME P)
(NOT (EQUAL (REMAINDER M P) 0))
(LESSP N P))
(ALL-DISTINCT (S N M P))).
This simplifies, opening up the functions ZEROP, PRIME, EQUAL,
LESSP, S, and ALL-DISTINCT, to:
T.
Case 2. (IMPLIES (AND (NOT (ZEROP N))
( LEQ P (SUB1 N))
(PRIME P)
(NOT (EQUAL (REMAINDER M P) 0))
(LESSP N P))
(ALL-DISTINCT (S N M P))).
This simplifies, using linear arithmetic, to the conjecture:
(IMPLIES (AND (LESSP N 1)
(NOT (ZEROP N))
( LEQ P (SUB1 N))
(PRIME P)
(NOT (EQUAL (REMAINDER M P) 0))
(LESSP N P))
(ALL-DISTINCT (S N M P))),
which we again simplify, expanding the functions SUB1, NUMBERP,
EQUAL, LESSP, and ZEROP, to:
T.
Case 1. (IMPLIES (AND (NOT (ZEROP N))
(ALL-DISTINCT (S (SUB1 N) M P))
(PRIME P)
(NOT (EQUAL (REMAINDER M P) 0))
(LESSP N P))
(ALL-DISTINCT (S N M P))),
which we simplify, using linear arithmetic, applying the lemmas
ALL-DISTINCT-S-LEMMA, CDR-CONS, and CAR-CONS, and opening up the
definitions of ZEROP, PRIME, S, and ALL-DISTINCT, to:
T.
That finishes the proof of *1. Q.E.D.
[ 76.03099 0.832006834 ]
ALL-DISTINCT-S
(PROVE-LEMMA ALL-NON-ZEROP-S
(REWRITE)
(IMPLIES (AND (PRIME P)
(NOT (EQUAL (REMAINDER M P) 0.))
(LESSP N P))
(ALL-NON-ZEROP (S N M P))))
This conjecture can be simplified, using the abbreviations NOT, PRIME,
AND, and IMPLIES, to:
(IMPLIES (AND (NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(NOT (EQUAL (REMAINDER M P) 0))
(LESSP N P))
(ALL-NON-ZEROP (S N M P))).
Appealing to the lemma REMAINDER-QUOTIENT-ELIM, replace M by
(PLUS X (TIMES P Z)) to eliminate (REMAINDER M P) and (QUOTIENT M P).
We rely upon LESSP-REMAINDER2, the type restriction lemma noted when
REMAINDER was introduced, and the type restriction lemma noted when
QUOTIENT was introduced to constrain the new variables. The result
is two new goals:
Case 2. (IMPLIES (AND (NOT (NUMBERP M))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(NOT (EQUAL (REMAINDER M P) 0))
(LESSP N P))
(ALL-NON-ZEROP (S N M P))),
which we simplify, unfolding LESSP, REMAINDER, and EQUAL, to:
T.
Case 1. (IMPLIES (AND (NUMBERP X)
(EQUAL (LESSP X P) (NOT (ZEROP P)))
(NUMBERP Z)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(NOT (EQUAL X 0))
(LESSP N P))
(ALL-NON-ZEROP (S N (PLUS X (TIMES P Z)) P))),
which simplifies, expanding the definitions of ZEROP and NOT, to:
(IMPLIES (AND (NUMBERP X)
(LESSP X P)
(NUMBERP Z)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(NOT (EQUAL X 0))
(LESSP N P))
(ALL-NON-ZEROP (S N (PLUS X (TIMES P Z)) P))).
Applying the lemma SUB1-ELIM, replace P by (ADD1 V) to eliminate
(SUB1 P). We employ the type restriction lemma noted when SUB1 was
introduced to constrain the new variable. We must thus prove:
(IMPLIES (AND (NUMBERP V)
(NUMBERP X)
(LESSP X (ADD1 V))
(NUMBERP Z)
(NOT (EQUAL (ADD1 V) 0))
(NOT (EQUAL (ADD1 V) 1))
(PRIME1 (ADD1 V) V)
(NOT (EQUAL X 0))
(LESSP N (ADD1 V)))
(ALL-NON-ZEROP (S N
(PLUS X (TIMES (ADD1 V) Z))
(ADD1 V)))).
But this further simplifies, rewriting with SUB1-ADD1, ADD1-EQUAL,
COMMUTATIVITY-OF-TIMES, and TIMES-ADD1, and expanding LESSP,
NUMBERP, EQUAL, S, and ALL-NON-ZEROP, to:
(IMPLIES (AND (NUMBERP V)
(NUMBERP X)
(LESSP (SUB1 X) V)
(NUMBERP Z)
(NOT (EQUAL V 0))
(PRIME1 (ADD1 V) V)
(NOT (EQUAL X 0))
(LESSP (SUB1 N) V))
(ALL-NON-ZEROP (S N
(PLUS X (PLUS Z (TIMES V Z)))
(ADD1 V)))).
Applying the lemma SUB1-ELIM, we now replace N by (ADD1 W) to
eliminate (SUB1 N). We employ the type restriction lemma noted
when SUB1 was introduced to constrain the new variable. The result
is three new conjectures:
Case 1.3.
(IMPLIES (AND (EQUAL N 0)
(NUMBERP V)
(NUMBERP X)
(LESSP (SUB1 X) V)
(NUMBERP Z)
(NOT (EQUAL V 0))
(PRIME1 (ADD1 V) V)
(NOT (EQUAL X 0))
(LESSP (SUB1 N) V))
(ALL-NON-ZEROP (S N
(PLUS X (PLUS Z (TIMES V Z)))
(ADD1 V)))),
which we finally simplify, unfolding SUB1, EQUAL, LESSP, S, and
ALL-NON-ZEROP, to:
T.
Case 1.2.
(IMPLIES (AND (NOT (NUMBERP N))
(NUMBERP V)
(NUMBERP X)
(LESSP (SUB1 X) V)
(NUMBERP Z)
(NOT (EQUAL V 0))
(PRIME1 (ADD1 V) V)
(NOT (EQUAL X 0))
(LESSP (SUB1 N) V))
(ALL-NON-ZEROP (S N
(PLUS X (PLUS Z (TIMES V Z)))
(ADD1 V)))),
which finally simplifies, rewriting with SUB1-NNUMBERP, and
expanding the definitions of EQUAL, LESSP, S, and ALL-NON-ZEROP,
to:
T.
Case 1.1.
(IMPLIES (AND (NUMBERP W)
(NOT (EQUAL (ADD1 W) 0))
(NUMBERP V)
(NUMBERP X)
(LESSP (SUB1 X) V)
(NUMBERP Z)
(NOT (EQUAL V 0))
(PRIME1 (ADD1 V) V)
(NOT (EQUAL X 0))
(LESSP W V))
(ALL-NON-ZEROP (S (ADD1 W)
(PLUS X (PLUS Z (TIMES V Z)))
(ADD1 V)))).
However this further simplifies, rewriting with the lemmas
SUB1-ADD1, ASSOCIATIVITY-OF-PLUS, COMMUTATIVITY2-OF-PLUS,
COMMUTATIVITY2-OF-TIMES, DISTRIBUTIVITY-OF-TIMES-OVER-PLUS,
TIMES-ADD1, COMMUTATIVITY-OF-TIMES, CDR-CONS, and CAR-CONS, and
unfolding the definitions of S and ALL-NON-ZEROP, to two new
conjectures:
Case 1.1.2.
(IMPLIES
(AND (NUMBERP W)
(NUMBERP V)
(NUMBERP X)
(LESSP (SUB1 X) V)
(NUMBERP Z)
(NOT (EQUAL V 0))
(PRIME1 (ADD1 V) V)
(NOT (EQUAL X 0))
(LESSP W V))
(NOT
(EQUAL
(REMAINDER
(PLUS X
(PLUS Z
(PLUS (TIMES V Z)
(PLUS (TIMES W X)
(PLUS (TIMES W Z)
(TIMES V (TIMES W Z)))))))
(ADD1 V))
0))),
which we would normally push and work on later by induction.
But if we must use induction to prove the input conjecture, we
prefer to induct on the original formulation of the problem.
Thus we will disregard all that we have previously done, give
the name *1 to the original input, and work on it.
So now let us consider:
(IMPLIES (AND (PRIME P)
(NOT (EQUAL (REMAINDER M P) 0))
(LESSP N P))
(ALL-NON-ZEROP (S N M P))),
named *1. We will try to prove it by induction. Four inductions are
suggested by terms in the conjecture. They merge into three likely
candidate inductions. However, only one is unflawed. We will induct
according to the following scheme:
(AND (IMPLIES (ZEROP N) (P N M P))
(IMPLIES (AND (NOT (ZEROP N)) (P (SUB1 N) M P))
(P N M P))).
Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of
ZEROP inform us that the measure (COUNT N) decreases according to the
well-founded relation LESSP in each induction step of the scheme.
The above induction scheme leads to the following three new
conjectures:
Case 3. (IMPLIES (AND (ZEROP N)
(PRIME P)
(NOT (EQUAL (REMAINDER M P) 0))
(LESSP N P))
(ALL-NON-ZEROP (S N M P))).
This simplifies, opening up the functions ZEROP, PRIME, EQUAL,
LESSP, S, and ALL-NON-ZEROP, to:
T.
Case 2. (IMPLIES (AND (NOT (ZEROP N))
( LEQ P (SUB1 N))
(PRIME P)
(NOT (EQUAL (REMAINDER M P) 0))
(LESSP N P))
(ALL-NON-ZEROP (S N M P))).
This simplifies, using linear arithmetic, to the conjecture:
(IMPLIES (AND (LESSP N 1)
(NOT (ZEROP N))
( LEQ P (SUB1 N))
(PRIME P)
(NOT (EQUAL (REMAINDER M P) 0))
(LESSP N P))
(ALL-NON-ZEROP (S N M P))),
which we again simplify, expanding the functions SUB1, NUMBERP,
EQUAL, LESSP, and ZEROP, to:
T.
Case 1. (IMPLIES (AND (NOT (ZEROP N))
(ALL-NON-ZEROP (S (SUB1 N) M P))
(PRIME P)
(NOT (EQUAL (REMAINDER M P) 0))
(LESSP N P))
(ALL-NON-ZEROP (S N M P))),
which we simplify, applying the lemmas CDR-CONS, PRIME-KEY-REWRITE,
and CAR-CONS, and opening up the definitions of ZEROP, PRIME, S,
REMAINDER, and ALL-NON-ZEROP, to:
T.
That finishes the proof of *1. Q.E.D.
[ 375.027954 0.81704102 ]
ALL-NON-ZEROP-S
(PROVE-LEMMA ALL-LESSEQP-S
(REWRITE)
(IMPLIES (NOT (ZEROP P))
(ALL-LESSEQP (S N M P) (SUB1 P))))
This formula can be simplified, using the abbreviations ZEROP, NOT,
and IMPLIES, to:
(IMPLIES (AND (NOT (EQUAL P 0)) (NUMBERP P))
(ALL-LESSEQP (S N M P) (SUB1 P))).
Appealing to the lemma SUB1-ELIM, we now replace P by (ADD1 X) to
eliminate (SUB1 P). We rely upon the type restriction lemma noted
when SUB1 was introduced to restrict the new variable. This produces
the new conjecture:
(IMPLIES (AND (NUMBERP X)
(NOT (EQUAL (ADD1 X) 0)))
(ALL-LESSEQP (S N M (ADD1 X)) X)).
Of course, this simplifies, trivially, to:
(IMPLIES (NUMBERP X)
(ALL-LESSEQP (S N M (ADD1 X)) X)),
which we would normally push and work on later by induction. But if
we must use induction to prove the input conjecture, we prefer to
induct on the original formulation of the problem. Thus we will
disregard all that we have previously done, give the name *1 to the
original input, and work on it.
So now let us consider:
(IMPLIES (NOT (ZEROP P))
(ALL-LESSEQP (S N M P) (SUB1 P))),
named *1. We will try to prove it by induction. There is only one
plausible induction. We will induct according to the following
scheme:
(AND (IMPLIES (ZEROP N) (P N M P))
(IMPLIES (AND (NOT (ZEROP N)) (P (SUB1 N) M P))
(P N M P))).
Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of
ZEROP can be used to establish that the measure (COUNT N) decreases
according to the well-founded relation LESSP in each induction step
of the scheme. The above induction scheme produces the following two
new goals:
Case 2. (IMPLIES (AND (ZEROP N) (NOT (ZEROP P)))
(ALL-LESSEQP (S N M P) (SUB1 P))),
which simplifies, rewriting with PIGEON-HOLE-PRINCIPLE-LEMMA-2 and
ADD1-SUB1, and expanding ZEROP, EQUAL, S, ALL-LESSEQP, MEMBER, and
LISTP, to:
T.
Case 1. (IMPLIES (AND (NOT (ZEROP N))
(ALL-LESSEQP (S (SUB1 N) M P)
(SUB1 P))
(NOT (ZEROP P)))
(ALL-LESSEQP (S N M P) (SUB1 P))),
which we simplify, applying CDR-CONS and CAR-CONS, and expanding
the definitions of ZEROP, S, and ALL-LESSEQP, to:
(IMPLIES (AND (NOT (EQUAL N 0))
(NUMBERP N)
(ALL-LESSEQP (S (SUB1 N) M P)
(SUB1 P))
(NOT (EQUAL P 0))
(NUMBERP P))
( LEQ
(REMAINDER (TIMES M N) P)
(SUB1 P))),
which we again simplify, using linear arithmetic and rewriting with
LESSP-REMAINDER-DIVISOR, to:
T.
That finishes the proof of *1. Q.E.D.
[ 6.8119792 0.32801107 ]
ALL-LESSEQP-S
(PROVE-LEMMA LENGTH-S
(REWRITE)
(EQUAL (LENGTH (S N M P)) (FIX N)))
This simplifies, opening up the function FIX, to the following two
new goals:
Case 2. (IMPLIES (NOT (NUMBERP N))
(EQUAL (LENGTH (S N M P)) 0)),
which again simplifies, opening up the definitions of S, LENGTH,
and EQUAL, to:
T.
Case 1. (IMPLIES (NUMBERP N)
(EQUAL (LENGTH (S N M P)) N)),
which we will name *1.
Perhaps we can prove it by induction. There is only one
plausible induction. We will induct according to the following
scheme:
(AND (IMPLIES (ZEROP N) (P N M P))
(IMPLIES (AND (NOT (ZEROP N)) (P (SUB1 N) M P))
(P N M P))).
Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of
ZEROP inform us that the measure (COUNT N) decreases according to the
well-founded relation LESSP in each induction step of the scheme.
The above induction scheme produces two new formulas:
Case 2. (IMPLIES (AND (ZEROP N) (NUMBERP N))
(EQUAL (LENGTH (S N M P)) N)).
This simplifies, opening up the definitions of ZEROP, NUMBERP,
EQUAL, S, and LENGTH, to:
T.
Case 1. (IMPLIES (AND (NOT (ZEROP N))
(EQUAL (LENGTH (S (SUB1 N) M P))
(SUB1 N))
(NUMBERP N))
(EQUAL (LENGTH (S N M P)) N)),
which we simplify, rewriting with the lemmas ADD1-SUB1 and CDR-CONS,
and unfolding the functions ZEROP, S, and LENGTH, to:
T.
That finishes the proof of *1. Q.E.D.
[ 2.16697592 0.202001953 ]
LENGTH-S
(PROVE-LEMMA FERMAT-THM
(REWRITE)
(IMPLIES (AND (PRIME P)
(NOT (EQUAL (REMAINDER M P) 0.)))
(EQUAL (REMAINDER (EXP M (SUB1 P)) P)
1.))
((USE (PIGEON-HOLE-PRINCIPLE (L (S (SUB1 P) M P)))
(REMAINDER-TIMES-LIST-S (N (SUB1 P))))
(DISABLE PIGEON-HOLE-PRINCIPLE REMAINDER-TIMES-LIST-S)))
This formula can be simplified, using the abbreviations NOT, PRIME,
IMPLIES, and AND, to:
(IMPLIES
(AND
(IMPLIES (AND (ALL-NON-ZEROP (S (SUB1 P) M P))
(AND (ALL-DISTINCT (S (SUB1 P) M P))
(ALL-LESSEQP (S (SUB1 P) M P)
(LENGTH (S (SUB1 P) M P)))))
(PERM (POSITIVES (LENGTH (S (SUB1 P) M P)))
(S (SUB1 P) M P)))
(EQUAL (REMAINDER (TIMES-LIST (S (SUB1 P) M P))
P)
(REMAINDER (TIMES (FACT (SUB1 P))
(EXP M (SUB1 P)))
P))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(NOT (EQUAL (REMAINDER M P) 0)))
(EQUAL (REMAINDER (EXP M (SUB1 P)) P)
1)).
This simplifies, using linear arithmetic, applying ALL-NON-ZEROP-S,
ALL-DISTINCT-S, LENGTH-S, ALL-LESSEQP-S, TIMES-LIST-EQUAL-FACT,
PRIME-FACT, and COROLLARY-55, and expanding PRIME, AND, and IMPLIES,
to:
T.
Q.E.D.
[ 15.4889973 0.098014323 ]
FERMAT-THM
(PROVE-LEMMA CRYPT-INVERTS-STEP-1 NIL
(IMPLIES (PRIME P)
(EQUAL (REMAINDER (TIMES M (EXP M (TIMES K (SUB1 P))))
P)
(REMAINDER M P))))
This conjecture can be simplified, using the abbreviations PRIME and
IMPLIES, to the new formula:
(IMPLIES (AND (NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P)))
(EQUAL (REMAINDER (TIMES M (EXP M (TIMES K (SUB1 P))))
P)
(REMAINDER M P))).
This simplifies, applying FERMAT-THM, EXP-MOD-IS-1, and COROLLARY-55,
and expanding PRIME and EQUAL, to:
T.
Q.E.D.
[ 5.17197263 0.055013021 ]
CRYPT-INVERTS-STEP-1
(PROVE-LEMMA CRYPT-INVERTS-STEP-1A
(REWRITE)
(IMPLIES
(PRIME P)
(EQUAL (REMAINDER (TIMES M
(EXP M (TIMES K (SUB1 P) (SUB1 Q))))
P)
(REMAINDER M P)))
((USE (CRYPT-INVERTS-STEP-1 (K (TIMES K (SUB1 Q)))))
(DISABLE CRYPT-INVERTS-STEP-1)))
This formula can be simplified, using the abbreviations PRIME,
IMPLIES, and ASSOCIATIVITY-OF-TIMES, to:
(IMPLIES
(AND
(IMPLIES
(PRIME P)
(EQUAL
(REMAINDER (TIMES M
(EXP M
(TIMES K (TIMES (SUB1 Q) (SUB1 P)))))
P)
(REMAINDER M P)))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P)))
(EQUAL
(REMAINDER (TIMES M
(EXP M
(TIMES K (TIMES (SUB1 P) (SUB1 Q)))))
P)
(REMAINDER M P))),
which simplifies, applying the lemmas COMMUTATIVITY-OF-TIMES,
COROLLARY-55, and PRIME-KEY-REWRITE, and unfolding PRIME, IMPLIES,
and EQUAL, to:
T.
Q.E.D.
[ 22.4989908 0.070019531 ]
CRYPT-INVERTS-STEP-1A
(PROVE-LEMMA CRYPT-INVERTS-STEP-1B
(REWRITE)
(IMPLIES
(PRIME Q)
(EQUAL (REMAINDER (TIMES M
(EXP M (TIMES K (SUB1 P) (SUB1 Q))))
Q)
(REMAINDER M Q)))
((USE (CRYPT-INVERTS-STEP-1 (P Q)
(K (TIMES K (SUB1 P)))))
(DISABLE CRYPT-INVERTS-STEP-1)))
This formula can be simplified, using the abbreviations PRIME,
IMPLIES, and ASSOCIATIVITY-OF-TIMES, to:
(IMPLIES
(AND
(IMPLIES
(PRIME Q)
(EQUAL
(REMAINDER (TIMES M
(EXP M
(TIMES K (TIMES (SUB1 P) (SUB1 Q)))))
Q)
(REMAINDER M Q)))
(NOT (EQUAL Q 0))
(NUMBERP Q)
(NOT (EQUAL Q 1))
(PRIME1 Q (SUB1 Q)))
(EQUAL
(REMAINDER (TIMES M
(EXP M
(TIMES K (TIMES (SUB1 P) (SUB1 Q)))))
Q)
(REMAINDER M Q))),
which simplifies, applying the lemmas EXP-MOD-IS-1, FERMAT-THM, and
COROLLARY-55, and unfolding PRIME, EQUAL, and IMPLIES, to:
T.
Q.E.D.
[ 10.0489908 0.87200521 ]
CRYPT-INVERTS-STEP-1B
(PROVE-LEMMA CRYPT-INVERTS-STEP-2
(REWRITE)
(IMPLIES (AND (PRIME P)
(PRIME Q)
(NOT (EQUAL P Q))
(NUMBERP M)
(LESSP M (TIMES P Q))
(EQUAL (REMAINDER ED
(TIMES (SUB1 P) (SUB1 Q)))
1.))
(EQUAL (REMAINDER (EXP M ED) (TIMES P Q))
M)))
This formula can be simplified, using the abbreviations NOT, PRIME,
AND, and IMPLIES, to:
(IMPLIES (AND (NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(NOT (EQUAL Q 0))
(NUMBERP Q)
(NOT (EQUAL Q 1))
(PRIME1 Q (SUB1 Q))
(NOT (EQUAL P Q))
(NUMBERP M)
(LESSP M (TIMES P Q))
(EQUAL (REMAINDER ED
(TIMES (SUB1 P) (SUB1 Q)))
1))
(EQUAL (REMAINDER (EXP M ED) (TIMES P Q))
M)).
Appealing to the lemma REMAINDER-QUOTIENT-ELIM, we now replace ED by:
(PLUS X
(TIMES (TIMES (SUB1 P) (SUB1 Q)) Z))
to eliminate (REMAINDER ED (TIMES (SUB1 P) (SUB1 Q))) and:
(QUOTIENT ED
(TIMES (SUB1 P) (SUB1 Q)))
. We use LESSP-REMAINDER2, the type restriction lemma noted when
REMAINDER was introduced, and the type restriction lemma noted when
QUOTIENT was introduced to constrain the new variables. We would
thus like to prove the following four new formulas:
Case 4. (IMPLIES (AND (NOT (NUMBERP ED))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(NOT (EQUAL Q 0))
(NUMBERP Q)
(NOT (EQUAL Q 1))
(PRIME1 Q (SUB1 Q))
(NOT (EQUAL P Q))
(NUMBERP M)
(LESSP M (TIMES P Q))
(EQUAL (REMAINDER ED
(TIMES (SUB1 P) (SUB1 Q)))
1))
(EQUAL (REMAINDER (EXP M ED) (TIMES P Q))
M)),
which simplifies, applying EQUAL-TIMES-0, and expanding the
definitions of LESSP, REMAINDER, and EQUAL, to:
T.
Case 3. (IMPLIES (AND (EQUAL (TIMES (SUB1 P) (SUB1 Q)) 0)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(NOT (EQUAL Q 0))
(NUMBERP Q)
(NOT (EQUAL Q 1))
(PRIME1 Q (SUB1 Q))
(NOT (EQUAL P Q))
(NUMBERP M)
(LESSP M (TIMES P Q))
(EQUAL (REMAINDER ED
(TIMES (SUB1 P) (SUB1 Q)))
1))
(EQUAL (REMAINDER (EXP M ED) (TIMES P Q))
M)),
which simplifies, using linear arithmetic and rewriting with
LESSP-TIMES-2, to:
T.
Case 2. (IMPLIES (AND (NOT (NUMBERP (TIMES (SUB1 P) (SUB1 Q))))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(NOT (EQUAL Q 0))
(NUMBERP Q)
(NOT (EQUAL Q 1))
(PRIME1 Q (SUB1 Q))
(NOT (EQUAL P Q))
(NUMBERP M)
(LESSP M (TIMES P Q))
(EQUAL (REMAINDER ED
(TIMES (SUB1 P) (SUB1 Q)))
1))
(EQUAL (REMAINDER (EXP M ED) (TIMES P Q))
M)),
which simplifies, obviously, to:
T.
Case 1. (IMPLIES
(AND (NUMBERP X)
(EQUAL (LESSP X (TIMES (SUB1 P) (SUB1 Q)))
(NOT (ZEROP (TIMES (SUB1 P) (SUB1 Q)))))
(NUMBERP Z)
(NOT (EQUAL (TIMES (SUB1 P) (SUB1 Q)) 0))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(NOT (EQUAL Q 0))
(NUMBERP Q)
(NOT (EQUAL Q 1))
(PRIME1 Q (SUB1 Q))
(NOT (EQUAL P Q))
(NUMBERP M)
(LESSP M (TIMES P Q))
(EQUAL X 1))
(EQUAL
(REMAINDER (EXP M
(PLUS X
(TIMES (TIMES (SUB1 P) (SUB1 Q)) Z)))
(TIMES P Q))
M)).
But this simplifies, rewriting with EQUAL-TIMES-0, EQUAL-LESSP,
COMMUTATIVITY-OF-TIMES, TIMES-IDENTITY, COMMUTATIVITY2-OF-TIMES,
ASSOCIATIVITY-OF-TIMES, TIMES-1, EXP-BY-0, EXP-PLUS,
CRYPT-INVERTS-STEP-1B, CRYPT-INVERTS-STEP-1A, and COROLLARY-53, and
expanding NUMBERP, ZEROP, NOT, EQUAL, SUB1, EXP, and PRIME, to:
T.
Q.E.D.
[ 46.0520506 0.398958333 ]
CRYPT-INVERTS-STEP-2
(PROVE-LEMMA CRYPT-INVERTS NIL
(IMPLIES (AND (PRIME P)
(PRIME Q)
(NOT (EQUAL P Q))
(EQUAL N (TIMES P Q))
(NUMBERP M)
(LESSP M N)
(EQUAL (REMAINDER (TIMES E D)
(TIMES (SUB1 P) (SUB1 Q)))
1.))
(EQUAL (CRYPT (CRYPT M E N) D N) M))
NIL)
This conjecture can be simplified, using the abbreviations NOT, PRIME,
AND, and IMPLIES, to the new formula:
(IMPLIES (AND (NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(NOT (EQUAL Q 0))
(NUMBERP Q)
(NOT (EQUAL Q 1))
(PRIME1 Q (SUB1 Q))
(NOT (EQUAL P Q))
(EQUAL N (TIMES P Q))
(NUMBERP M)
(LESSP M N)
(EQUAL (REMAINDER (TIMES E D)
(TIMES (SUB1 P) (SUB1 Q)))
1))
(EQUAL (CRYPT (CRYPT M E N) D N) M)).
This simplifies, using linear arithmetic, applying
COMMUTATIVITY-OF-TIMES, LESSP-TIMES-1, CRYPT-CORRECT, EXP-EXP,
CRYPT-INVERTS-STEP-2, and REMAINDER-EXP, and expanding PRIME, to:
T.
Q.E.D.
[ 42.3430176 0.123990885 ]
CRYPT-INVERTS
SYSTEM
[ 0.0 0.0 ]BASIS.LISP.
GENFACT.LISP.
EVENTS.LISP.
CODE-1-A.LISP.
CODE-B-D.LISP.
CODE-E-M.LISP.
CODE-N-R.LISP.
CODE-S-Z.LISP.
IO.LISP.
PPR.LISP.
Maclisp Version 2133
REDO-UNDONE-EVENTS completed. Here is FAILED-THMS:
NIL